Proof of Theorem dmdprdpr
| Step | Hyp | Ref
| Expression |
| 1 | | 0ex 5307 |
. . . . . 6
⊢ ∅
∈ V |
| 2 | | dmdprdpr.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) |
| 3 | | dprdsn 20056 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝑆 ∈
(SubGrp‘𝐺)) →
(𝐺dom DProd {〈∅,
𝑆〉} ∧ (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆)) |
| 4 | 1, 2, 3 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉} ∧ (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆)) |
| 5 | 4 | simpld 494 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd {〈∅, 𝑆〉}) |
| 6 | | dmdprdpr.t |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
| 7 | | xpscf 17610 |
. . . . . . . 8
⊢
({〈∅, 𝑆〉, 〈1o, 𝑇〉}:2o⟶(SubGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺))) |
| 8 | 2, 6, 7 | sylanbrc 583 |
. . . . . . 7
⊢ (𝜑 → {〈∅, 𝑆〉, 〈1o,
𝑇〉}:2o⟶(SubGrp‘𝐺)) |
| 9 | 8 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → {〈∅, 𝑆〉, 〈1o,
𝑇〉} Fn
2o) |
| 10 | 1 | prid1 4762 |
. . . . . . 7
⊢ ∅
∈ {∅, 1o} |
| 11 | | df2o3 8514 |
. . . . . . 7
⊢
2o = {∅, 1o} |
| 12 | 10, 11 | eleqtrri 2840 |
. . . . . 6
⊢ ∅
∈ 2o |
| 13 | | fnressn 7178 |
. . . . . 6
⊢
(({〈∅, 𝑆〉, 〈1o, 𝑇〉} Fn 2o ∧
∅ ∈ 2o) → ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}) =
{〈∅, ({〈∅, 𝑆〉, 〈1o, 𝑇〉}‘∅)〉}) |
| 14 | 9, 12, 13 | sylancl 586 |
. . . . 5
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾ {∅})
= {〈∅, ({〈∅, 𝑆〉, 〈1o, 𝑇〉}‘∅)〉}) |
| 15 | | fvpr0o 17604 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ({〈∅, 𝑆〉, 〈1o,
𝑇〉}‘∅) =
𝑆) |
| 16 | 2, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉}‘∅) =
𝑆) |
| 17 | 16 | opeq2d 4880 |
. . . . . 6
⊢ (𝜑 → 〈∅,
({〈∅, 𝑆〉,
〈1o, 𝑇〉}‘∅)〉 =
〈∅, 𝑆〉) |
| 18 | 17 | sneqd 4638 |
. . . . 5
⊢ (𝜑 → {〈∅,
({〈∅, 𝑆〉,
〈1o, 𝑇〉}‘∅)〉} =
{〈∅, 𝑆〉}) |
| 19 | 14, 18 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾ {∅})
= {〈∅, 𝑆〉}) |
| 20 | 5, 19 | breqtrrd 5171 |
. . 3
⊢ (𝜑 → 𝐺dom DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{∅})) |
| 21 | | 1on 8518 |
. . . . . 6
⊢
1o ∈ On |
| 22 | | dprdsn 20056 |
. . . . . 6
⊢
((1o ∈ On ∧ 𝑇 ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈1o, 𝑇〉} ∧ (𝐺 DProd {〈1o, 𝑇〉}) = 𝑇)) |
| 23 | 21, 6, 22 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈1o, 𝑇〉} ∧ (𝐺 DProd {〈1o, 𝑇〉}) = 𝑇)) |
| 24 | 23 | simpld 494 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd {〈1o, 𝑇〉}) |
| 25 | | 1oex 8516 |
. . . . . . . 8
⊢
1o ∈ V |
| 26 | 25 | prid2 4763 |
. . . . . . 7
⊢
1o ∈ {∅, 1o} |
| 27 | 26, 11 | eleqtrri 2840 |
. . . . . 6
⊢
1o ∈ 2o |
| 28 | | fnressn 7178 |
. . . . . 6
⊢
(({〈∅, 𝑆〉, 〈1o, 𝑇〉} Fn 2o ∧
1o ∈ 2o) → ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {1o})
= {〈1o, ({〈∅, 𝑆〉, 〈1o, 𝑇〉}‘1o)〉}) |
| 29 | 9, 27, 28 | sylancl 586 |
. . . . 5
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{1o}) = {〈1o, ({〈∅, 𝑆〉, 〈1o, 𝑇〉}‘1o)〉}) |
| 30 | | fvpr1o 17605 |
. . . . . . . 8
⊢ (𝑇 ∈ (SubGrp‘𝐺) → ({〈∅, 𝑆〉, 〈1o,
𝑇〉}‘1o) = 𝑇) |
| 31 | 6, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉}‘1o) = 𝑇) |
| 32 | 31 | opeq2d 4880 |
. . . . . 6
⊢ (𝜑 → 〈1o,
({〈∅, 𝑆〉,
〈1o, 𝑇〉}‘1o)〉 =
〈1o, 𝑇〉) |
| 33 | 32 | sneqd 4638 |
. . . . 5
⊢ (𝜑 → {〈1o,
({〈∅, 𝑆〉,
〈1o, 𝑇〉}‘1o)〉} =
{〈1o, 𝑇〉}) |
| 34 | 29, 33 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{1o}) = {〈1o, 𝑇〉}) |
| 35 | 24, 34 | breqtrrd 5171 |
. . 3
⊢ (𝜑 → 𝐺dom DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{1o})) |
| 36 | | 1n0 8526 |
. . . . . . . . 9
⊢
1o ≠ ∅ |
| 37 | 36 | necomi 2995 |
. . . . . . . 8
⊢ ∅
≠ 1o |
| 38 | | disjsn2 4712 |
. . . . . . . 8
⊢ (∅
≠ 1o → ({∅} ∩ {1o}) =
∅) |
| 39 | 37, 38 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ({∅} ∩
{1o}) = ∅) |
| 40 | | df-pr 4629 |
. . . . . . . . 9
⊢ {∅,
1o} = ({∅} ∪ {1o}) |
| 41 | 11, 40 | eqtri 2765 |
. . . . . . . 8
⊢
2o = ({∅} ∪ {1o}) |
| 42 | 41 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2o = ({∅}
∪ {1o})) |
| 43 | | dmdprdpr.z |
. . . . . . 7
⊢ 𝑍 = (Cntz‘𝐺) |
| 44 | | dmdprdpr.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
| 45 | 8, 39, 42, 43, 44 | dmdprdsplit 20067 |
. . . . . 6
⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉} ↔ ((𝐺dom DProd ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾ {∅})
∧ 𝐺dom DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o})) ∧
(𝐺 DProd ({〈∅,
𝑆〉,
〈1o, 𝑇〉} ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{1o}))) ∧ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
∩ (𝐺 DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = { 0
}))) |
| 46 | | 3anass 1095 |
. . . . . 6
⊢ (((𝐺dom DProd ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾ {∅})
∧ 𝐺dom DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o})) ∧
(𝐺 DProd ({〈∅,
𝑆〉,
〈1o, 𝑇〉} ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{1o}))) ∧ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
∩ (𝐺 DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = { 0 }) ↔
((𝐺dom DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {∅}) ∧ 𝐺dom DProd ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{1o})) ∧ ((𝐺
DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
⊆ (𝑍‘(𝐺 DProd ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{1o}))) ∧ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
∩ (𝐺 DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = { 0
}))) |
| 47 | 45, 46 | bitrdi 287 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉} ↔ ((𝐺dom DProd ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾ {∅})
∧ 𝐺dom DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o})) ∧
((𝐺 DProd ({〈∅,
𝑆〉,
〈1o, 𝑇〉} ↾ {∅})) ⊆ (𝑍‘(𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{1o}))) ∧ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
∩ (𝐺 DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = { 0
})))) |
| 48 | 47 | baibd 539 |
. . . 4
⊢ ((𝜑 ∧ (𝐺dom DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}) ∧
𝐺dom DProd ({〈∅,
𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) →
(𝐺dom DProd {〈∅,
𝑆〉,
〈1o, 𝑇〉} ↔ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
⊆ (𝑍‘(𝐺 DProd ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{1o}))) ∧ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
∩ (𝐺 DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = { 0
}))) |
| 49 | 48 | ex 412 |
. . 3
⊢ (𝜑 → ((𝐺dom DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}) ∧
𝐺dom DProd ({〈∅,
𝑆〉,
〈1o, 𝑇〉} ↾ {1o})) →
(𝐺dom DProd {〈∅,
𝑆〉,
〈1o, 𝑇〉} ↔ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
⊆ (𝑍‘(𝐺 DProd ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{1o}))) ∧ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
∩ (𝐺 DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = { 0
})))) |
| 50 | 20, 35, 49 | mp2and 699 |
. 2
⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉} ↔ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{∅})) ⊆ (𝑍‘(𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{1o}))) ∧ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
∩ (𝐺 DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = { 0
}))) |
| 51 | 19 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅})) =
(𝐺 DProd {〈∅,
𝑆〉})) |
| 52 | 4 | simprd 495 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆) |
| 53 | 51, 52 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅})) =
𝑆) |
| 54 | 34 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{1o})) = (𝐺
DProd {〈1o, 𝑇〉})) |
| 55 | 23 | simprd 495 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd {〈1o, 𝑇〉}) = 𝑇) |
| 56 | 54, 55 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{1o})) = 𝑇) |
| 57 | 56 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (𝑍‘(𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{1o}))) = (𝑍‘𝑇)) |
| 58 | 53, 57 | sseq12d 4017 |
. . 3
⊢ (𝜑 → ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
⊆ (𝑍‘(𝐺 DProd ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{1o}))) ↔ 𝑆
⊆ (𝑍‘𝑇))) |
| 59 | 53, 56 | ineq12d 4221 |
. . . 4
⊢ (𝜑 → ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
∩ (𝐺 DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = (𝑆 ∩ 𝑇)) |
| 60 | 59 | eqeq1d 2739 |
. . 3
⊢ (𝜑 → (((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
∩ (𝐺 DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = { 0 } ↔
(𝑆 ∩ 𝑇) = { 0 })) |
| 61 | 58, 60 | anbi12d 632 |
. 2
⊢ (𝜑 → (((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
⊆ (𝑍‘(𝐺 DProd ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{1o}))) ∧ ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
∩ (𝐺 DProd
({〈∅, 𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = { 0 }) ↔
(𝑆 ⊆ (𝑍‘𝑇) ∧ (𝑆 ∩ 𝑇) = { 0 }))) |
| 62 | 50, 61 | bitrd 279 |
1
⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉} ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ (𝑆 ∩ 𝑇) = { 0 }))) |