Proof of Theorem dprdpr
Step | Hyp | Ref
| Expression |
1 | | dmdprdpr.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) |
2 | | dmdprdpr.t |
. . . 4
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
3 | | xpscf 17276 |
. . . 4
⊢
({〈∅, 𝑆〉, 〈1o, 𝑇〉}:2o⟶(SubGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺))) |
4 | 1, 2, 3 | sylanbrc 583 |
. . 3
⊢ (𝜑 → {〈∅, 𝑆〉, 〈1o,
𝑇〉}:2o⟶(SubGrp‘𝐺)) |
5 | | 1n0 8318 |
. . . . 5
⊢
1o ≠ ∅ |
6 | 5 | necomi 2998 |
. . . 4
⊢ ∅
≠ 1o |
7 | | disjsn2 4648 |
. . . 4
⊢ (∅
≠ 1o → ({∅} ∩ {1o}) =
∅) |
8 | 6, 7 | mp1i 13 |
. . 3
⊢ (𝜑 → ({∅} ∩
{1o}) = ∅) |
9 | | df2o3 8305 |
. . . . 5
⊢
2o = {∅, 1o} |
10 | | df-pr 4564 |
. . . . 5
⊢ {∅,
1o} = ({∅} ∪ {1o}) |
11 | 9, 10 | eqtri 2766 |
. . . 4
⊢
2o = ({∅} ∪ {1o}) |
12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → 2o = ({∅}
∪ {1o})) |
13 | | dprdpr.s |
. . 3
⊢ ⊕ =
(LSSum‘𝐺) |
14 | | dprdpr.1 |
. . . 4
⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑇)) |
15 | | dprdpr.2 |
. . . 4
⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 }) |
16 | | dmdprdpr.z |
. . . . 5
⊢ 𝑍 = (Cntz‘𝐺) |
17 | | dmdprdpr.0 |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
18 | 16, 17, 1, 2 | dmdprdpr 19652 |
. . . 4
⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉} ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ (𝑆 ∩ 𝑇) = { 0 }))) |
19 | 14, 15, 18 | mpbir2and 710 |
. . 3
⊢ (𝜑 → 𝐺dom DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉}) |
20 | 4, 8, 12, 13, 19 | dprdsplit 19651 |
. 2
⊢ (𝜑 → (𝐺 DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉}) = ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
⊕
(𝐺 DProd ({〈∅,
𝑆〉,
〈1o, 𝑇〉} ↾
{1o})))) |
21 | 4 | ffnd 6601 |
. . . . . . 7
⊢ (𝜑 → {〈∅, 𝑆〉, 〈1o,
𝑇〉} Fn
2o) |
22 | | 0ex 5231 |
. . . . . . . . 9
⊢ ∅
∈ V |
23 | 22 | prid1 4698 |
. . . . . . . 8
⊢ ∅
∈ {∅, 1o} |
24 | 23, 9 | eleqtrri 2838 |
. . . . . . 7
⊢ ∅
∈ 2o |
25 | | fnressn 7030 |
. . . . . . 7
⊢
(({〈∅, 𝑆〉, 〈1o, 𝑇〉} Fn 2o ∧
∅ ∈ 2o) → ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}) =
{〈∅, ({〈∅, 𝑆〉, 〈1o, 𝑇〉}‘∅)〉}) |
26 | 21, 24, 25 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾ {∅})
= {〈∅, ({〈∅, 𝑆〉, 〈1o, 𝑇〉}‘∅)〉}) |
27 | | fvpr0o 17270 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ({〈∅, 𝑆〉, 〈1o,
𝑇〉}‘∅) =
𝑆) |
28 | 1, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉}‘∅) =
𝑆) |
29 | 28 | opeq2d 4811 |
. . . . . . 7
⊢ (𝜑 → 〈∅,
({〈∅, 𝑆〉,
〈1o, 𝑇〉}‘∅)〉 =
〈∅, 𝑆〉) |
30 | 29 | sneqd 4573 |
. . . . . 6
⊢ (𝜑 → {〈∅,
({〈∅, 𝑆〉,
〈1o, 𝑇〉}‘∅)〉} =
{〈∅, 𝑆〉}) |
31 | 26, 30 | eqtrd 2778 |
. . . . 5
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾ {∅})
= {〈∅, 𝑆〉}) |
32 | 31 | oveq2d 7291 |
. . . 4
⊢ (𝜑 → (𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅})) =
(𝐺 DProd {〈∅,
𝑆〉})) |
33 | | dprdsn 19639 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝑆 ∈
(SubGrp‘𝐺)) →
(𝐺dom DProd {〈∅,
𝑆〉} ∧ (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆)) |
34 | 22, 1, 33 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉} ∧ (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆)) |
35 | 34 | simprd 496 |
. . . 4
⊢ (𝜑 → (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆) |
36 | 32, 35 | eqtrd 2778 |
. . 3
⊢ (𝜑 → (𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅})) =
𝑆) |
37 | | 1oex 8307 |
. . . . . . . . 9
⊢
1o ∈ V |
38 | 37 | prid2 4699 |
. . . . . . . 8
⊢
1o ∈ {∅, 1o} |
39 | 38, 9 | eleqtrri 2838 |
. . . . . . 7
⊢
1o ∈ 2o |
40 | | fnressn 7030 |
. . . . . . 7
⊢
(({〈∅, 𝑆〉, 〈1o, 𝑇〉} Fn 2o ∧
1o ∈ 2o) → ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {1o})
= {〈1o, ({〈∅, 𝑆〉, 〈1o, 𝑇〉}‘1o)〉}) |
41 | 21, 39, 40 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{1o}) = {〈1o, ({〈∅, 𝑆〉, 〈1o, 𝑇〉}‘1o)〉}) |
42 | | fvpr1o 17271 |
. . . . . . . . 9
⊢ (𝑇 ∈ (SubGrp‘𝐺) → ({〈∅, 𝑆〉, 〈1o,
𝑇〉}‘1o) = 𝑇) |
43 | 2, 42 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉}‘1o) = 𝑇) |
44 | 43 | opeq2d 4811 |
. . . . . . 7
⊢ (𝜑 → 〈1o,
({〈∅, 𝑆〉,
〈1o, 𝑇〉}‘1o)〉 =
〈1o, 𝑇〉) |
45 | 44 | sneqd 4573 |
. . . . . 6
⊢ (𝜑 → {〈1o,
({〈∅, 𝑆〉,
〈1o, 𝑇〉}‘1o)〉} =
{〈1o, 𝑇〉}) |
46 | 41, 45 | eqtrd 2778 |
. . . . 5
⊢ (𝜑 → ({〈∅, 𝑆〉, 〈1o,
𝑇〉} ↾
{1o}) = {〈1o, 𝑇〉}) |
47 | 46 | oveq2d 7291 |
. . . 4
⊢ (𝜑 → (𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{1o})) = (𝐺
DProd {〈1o, 𝑇〉})) |
48 | | 1on 8309 |
. . . . . 6
⊢
1o ∈ On |
49 | | dprdsn 19639 |
. . . . . 6
⊢
((1o ∈ On ∧ 𝑇 ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈1o, 𝑇〉} ∧ (𝐺 DProd {〈1o, 𝑇〉}) = 𝑇)) |
50 | 48, 2, 49 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈1o, 𝑇〉} ∧ (𝐺 DProd {〈1o, 𝑇〉}) = 𝑇)) |
51 | 50 | simprd 496 |
. . . 4
⊢ (𝜑 → (𝐺 DProd {〈1o, 𝑇〉}) = 𝑇) |
52 | 47, 51 | eqtrd 2778 |
. . 3
⊢ (𝜑 → (𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾
{1o})) = 𝑇) |
53 | 36, 52 | oveq12d 7293 |
. 2
⊢ (𝜑 → ((𝐺 DProd ({〈∅, 𝑆〉, 〈1o, 𝑇〉} ↾ {∅}))
⊕
(𝐺 DProd ({〈∅,
𝑆〉,
〈1o, 𝑇〉} ↾ {1o}))) = (𝑆 ⊕ 𝑇)) |
54 | 20, 53 | eqtrd 2778 |
1
⊢ (𝜑 → (𝐺 DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉}) = (𝑆 ⊕ 𝑇)) |