Proof of Theorem dmdprdpr
Step | Hyp | Ref
| Expression |
1 | | 0ex 4790 |
. . . . . 6
⊢ ∅
∈ V |
2 | | dmdprdpr.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) |
3 | | dprdsn 18435 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝑆 ∈
(SubGrp‘𝐺)) →
(𝐺dom DProd {〈∅,
𝑆〉} ∧ (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆)) |
4 | 1, 2, 3 | sylancr 695 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉} ∧ (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆)) |
5 | 4 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd {〈∅, 𝑆〉}) |
6 | | dmdprdpr.t |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
7 | | xpscf 16226 |
. . . . . . . 8
⊢ (◡({𝑆} +𝑐 {𝑇}):2𝑜⟶(SubGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺))) |
8 | 2, 6, 7 | sylanbrc 698 |
. . . . . . 7
⊢ (𝜑 → ◡({𝑆} +𝑐 {𝑇}):2𝑜⟶(SubGrp‘𝐺)) |
9 | | ffn 6045 |
. . . . . . 7
⊢ (◡({𝑆} +𝑐 {𝑇}):2𝑜⟶(SubGrp‘𝐺) → ◡({𝑆} +𝑐 {𝑇}) Fn 2𝑜) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → ◡({𝑆} +𝑐 {𝑇}) Fn
2𝑜) |
11 | 1 | prid1 4297 |
. . . . . . 7
⊢ ∅
∈ {∅, 1𝑜} |
12 | | df2o3 7573 |
. . . . . . 7
⊢
2𝑜 = {∅,
1𝑜} |
13 | 11, 12 | eleqtrri 2700 |
. . . . . 6
⊢ ∅
∈ 2𝑜 |
14 | | fnressn 6425 |
. . . . . 6
⊢ ((◡({𝑆} +𝑐 {𝑇}) Fn 2𝑜 ∧ ∅
∈ 2𝑜) → (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) = {〈∅,
(◡({𝑆} +𝑐 {𝑇})‘∅)〉}) |
15 | 10, 13, 14 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) = {〈∅,
(◡({𝑆} +𝑐 {𝑇})‘∅)〉}) |
16 | | xpsc0 16220 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (◡({𝑆} +𝑐 {𝑇})‘∅) = 𝑆) |
17 | 2, 16 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇})‘∅) = 𝑆) |
18 | 17 | opeq2d 4409 |
. . . . . 6
⊢ (𝜑 → 〈∅, (◡({𝑆} +𝑐 {𝑇})‘∅)〉 = 〈∅,
𝑆〉) |
19 | 18 | sneqd 4189 |
. . . . 5
⊢ (𝜑 → {〈∅, (◡({𝑆} +𝑐 {𝑇})‘∅)〉} = {〈∅,
𝑆〉}) |
20 | 15, 19 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) = {〈∅,
𝑆〉}) |
21 | 5, 20 | breqtrrd 4681 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) |
22 | | 1on 7567 |
. . . . . 6
⊢
1𝑜 ∈ On |
23 | | dprdsn 18435 |
. . . . . 6
⊢
((1𝑜 ∈ On ∧ 𝑇 ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈1𝑜,
𝑇〉} ∧ (𝐺 DProd
{〈1𝑜, 𝑇〉}) = 𝑇)) |
24 | 22, 6, 23 | sylancr 695 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈1𝑜,
𝑇〉} ∧ (𝐺 DProd
{〈1𝑜, 𝑇〉}) = 𝑇)) |
25 | 24 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd {〈1𝑜,
𝑇〉}) |
26 | 22 | elexi 3213 |
. . . . . . . 8
⊢
1𝑜 ∈ V |
27 | 26 | prid2 4298 |
. . . . . . 7
⊢
1𝑜 ∈ {∅,
1𝑜} |
28 | 27, 12 | eleqtrri 2700 |
. . . . . 6
⊢
1𝑜 ∈ 2𝑜 |
29 | | fnressn 6425 |
. . . . . 6
⊢ ((◡({𝑆} +𝑐 {𝑇}) Fn 2𝑜 ∧
1𝑜 ∈ 2𝑜) → (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}) =
{〈1𝑜, (◡({𝑆} +𝑐 {𝑇})‘1𝑜)〉}) |
30 | 10, 28, 29 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}) =
{〈1𝑜, (◡({𝑆} +𝑐 {𝑇})‘1𝑜)〉}) |
31 | | xpsc1 16221 |
. . . . . . . 8
⊢ (𝑇 ∈ (SubGrp‘𝐺) → (◡({𝑆} +𝑐 {𝑇})‘1𝑜) = 𝑇) |
32 | 6, 31 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇})‘1𝑜) = 𝑇) |
33 | 32 | opeq2d 4409 |
. . . . . 6
⊢ (𝜑 →
〈1𝑜, (◡({𝑆} +𝑐 {𝑇})‘1𝑜)〉 =
〈1𝑜, 𝑇〉) |
34 | 33 | sneqd 4189 |
. . . . 5
⊢ (𝜑 →
{〈1𝑜, (◡({𝑆} +𝑐 {𝑇})‘1𝑜)〉} =
{〈1𝑜, 𝑇〉}) |
35 | 30, 34 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}) =
{〈1𝑜, 𝑇〉}) |
36 | 25, 35 | breqtrrd 4681 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾
{1𝑜})) |
37 | | 1n0 7575 |
. . . . . . . . 9
⊢
1𝑜 ≠ ∅ |
38 | 37 | necomi 2848 |
. . . . . . . 8
⊢ ∅
≠ 1𝑜 |
39 | | disjsn2 4247 |
. . . . . . . 8
⊢ (∅
≠ 1𝑜 → ({∅} ∩ {1𝑜}) =
∅) |
40 | 38, 39 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ({∅} ∩
{1𝑜}) = ∅) |
41 | | df-pr 4180 |
. . . . . . . . 9
⊢ {∅,
1𝑜} = ({∅} ∪
{1𝑜}) |
42 | 12, 41 | eqtri 2644 |
. . . . . . . 8
⊢
2𝑜 = ({∅} ∪
{1𝑜}) |
43 | 42 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2𝑜 =
({∅} ∪ {1𝑜})) |
44 | | dmdprdpr.z |
. . . . . . 7
⊢ 𝑍 = (Cntz‘𝐺) |
45 | | dmdprdpr.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
46 | 8, 40, 43, 44, 45 | dmdprdsplit 18446 |
. . . . . 6
⊢ (𝜑 → (𝐺dom DProd ◡({𝑆} +𝑐 {𝑇}) ↔ ((𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) ∧ 𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜})) ∧
(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) ∧
((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ∩ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) = {
0
}))) |
47 | | 3anass 1042 |
. . . . . 6
⊢ (((𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) ∧ 𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜})) ∧
(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) ∧
((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ∩ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) = {
0 })
↔ ((𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) ∧ 𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜})) ∧
((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) ∧
((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ∩ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) = {
0
}))) |
48 | 46, 47 | syl6bb 276 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd ◡({𝑆} +𝑐 {𝑇}) ↔ ((𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) ∧ 𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜})) ∧
((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) ∧
((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ∩ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) = {
0
})))) |
49 | 48 | baibd 948 |
. . . 4
⊢ ((𝜑 ∧ (𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) ∧ 𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) →
(𝐺dom DProd ◡({𝑆} +𝑐 {𝑇}) ↔ ((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) ∧
((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ∩ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) = {
0
}))) |
50 | 49 | ex 450 |
. . 3
⊢ (𝜑 → ((𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) ∧ 𝐺dom DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜})) →
(𝐺dom DProd ◡({𝑆} +𝑐 {𝑇}) ↔ ((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) ∧
((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ∩ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) = {
0
})))) |
51 | 21, 36, 50 | mp2and 715 |
. 2
⊢ (𝜑 → (𝐺dom DProd ◡({𝑆} +𝑐 {𝑇}) ↔ ((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) ∧
((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ∩ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) = {
0
}))) |
52 | 20 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) = (𝐺 DProd {〈∅, 𝑆〉})) |
53 | 4 | simprd 479 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆) |
54 | 52, 53 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) = 𝑆) |
55 | 35 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜})) =
(𝐺 DProd
{〈1𝑜, 𝑇〉})) |
56 | 24 | simprd 479 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd {〈1𝑜, 𝑇〉}) = 𝑇) |
57 | 55, 56 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜})) = 𝑇) |
58 | 57 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (𝑍‘(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) =
(𝑍‘𝑇)) |
59 | 54, 58 | sseq12d 3634 |
. . 3
⊢ (𝜑 → ((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) ↔
𝑆 ⊆ (𝑍‘𝑇))) |
60 | 54, 57 | ineq12d 3815 |
. . . 4
⊢ (𝜑 → ((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ∩ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) =
(𝑆 ∩ 𝑇)) |
61 | 60 | eqeq1d 2624 |
. . 3
⊢ (𝜑 → (((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ∩ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) = {
0 }
↔ (𝑆 ∩ 𝑇) = { 0 })) |
62 | 59, 61 | anbi12d 747 |
. 2
⊢ (𝜑 → (((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) ∧
((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ∩ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) = {
0 })
↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ (𝑆 ∩ 𝑇) = { 0 }))) |
63 | 51, 62 | bitrd 268 |
1
⊢ (𝜑 → (𝐺dom DProd ◡({𝑆} +𝑐 {𝑇}) ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ (𝑆 ∩ 𝑇) = { 0 }))) |