Proof of Theorem dprdpr
Step | Hyp | Ref
| Expression |
1 | | dmdprdpr.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) |
2 | | dmdprdpr.t |
. . . 4
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
3 | | xpscf 16049 |
. . . 4
⊢ (◡({𝑆} +𝑐 {𝑇}):2𝑜⟶(SubGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺))) |
4 | 1, 2, 3 | sylanbrc 695 |
. . 3
⊢ (𝜑 → ◡({𝑆} +𝑐 {𝑇}):2𝑜⟶(SubGrp‘𝐺)) |
5 | | 1n0 7462 |
. . . . 5
⊢
1𝑜 ≠ ∅ |
6 | 5 | necomi 2836 |
. . . 4
⊢ ∅
≠ 1𝑜 |
7 | | disjsn2 4193 |
. . . 4
⊢ (∅
≠ 1𝑜 → ({∅} ∩ {1𝑜}) =
∅) |
8 | 6, 7 | mp1i 13 |
. . 3
⊢ (𝜑 → ({∅} ∩
{1𝑜}) = ∅) |
9 | | df2o3 7460 |
. . . . 5
⊢
2𝑜 = {∅,
1𝑜} |
10 | | df-pr 4128 |
. . . . 5
⊢ {∅,
1𝑜} = ({∅} ∪
{1𝑜}) |
11 | 9, 10 | eqtri 2632 |
. . . 4
⊢
2𝑜 = ({∅} ∪
{1𝑜}) |
12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → 2𝑜 =
({∅} ∪ {1𝑜})) |
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 18271 |
. . . 4
⊢ (𝜑 → (𝐺dom DProd ◡({𝑆} +𝑐 {𝑇}) ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ (𝑆 ∩ 𝑇) = { 0 }))) |
19 | 14, 15, 18 | mpbir2and 959 |
. . 3
⊢ (𝜑 → 𝐺dom DProd ◡({𝑆} +𝑐 {𝑇})) |
20 | 4, 8, 12, 13, 19 | dprdsplit 18270 |
. 2
⊢ (𝜑 → (𝐺 DProd ◡({𝑆} +𝑐 {𝑇})) = ((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊕ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾
{1𝑜})))) |
21 | | ffn 5958 |
. . . . . . . 8
⊢ (◡({𝑆} +𝑐 {𝑇}):2𝑜⟶(SubGrp‘𝐺) → ◡({𝑆} +𝑐 {𝑇}) Fn 2𝑜) |
22 | 4, 21 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ◡({𝑆} +𝑐 {𝑇}) Fn
2𝑜) |
23 | | 0ex 4718 |
. . . . . . . . 9
⊢ ∅
∈ V |
24 | 23 | prid1 4241 |
. . . . . . . 8
⊢ ∅
∈ {∅, 1𝑜} |
25 | 24, 9 | eleqtrri 2687 |
. . . . . . 7
⊢ ∅
∈ 2𝑜 |
26 | | fnressn 6330 |
. . . . . . 7
⊢ ((◡({𝑆} +𝑐 {𝑇}) Fn 2𝑜 ∧ ∅
∈ 2𝑜) → (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) = {〈∅,
(◡({𝑆} +𝑐 {𝑇})‘∅)〉}) |
27 | 22, 25, 26 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) = {〈∅,
(◡({𝑆} +𝑐 {𝑇})‘∅)〉}) |
28 | | xpsc0 16043 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (◡({𝑆} +𝑐 {𝑇})‘∅) = 𝑆) |
29 | 1, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇})‘∅) = 𝑆) |
30 | 29 | opeq2d 4347 |
. . . . . . 7
⊢ (𝜑 → 〈∅, (◡({𝑆} +𝑐 {𝑇})‘∅)〉 = 〈∅,
𝑆〉) |
31 | 30 | sneqd 4137 |
. . . . . 6
⊢ (𝜑 → {〈∅, (◡({𝑆} +𝑐 {𝑇})‘∅)〉} = {〈∅,
𝑆〉}) |
32 | 27, 31 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇}) ↾ {∅}) = {〈∅,
𝑆〉}) |
33 | 32 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) = (𝐺 DProd {〈∅, 𝑆〉})) |
34 | | dprdsn 18258 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝑆 ∈
(SubGrp‘𝐺)) →
(𝐺dom DProd {〈∅,
𝑆〉} ∧ (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆)) |
35 | 23, 1, 34 | sylancr 694 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉} ∧ (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆)) |
36 | 35 | simprd 478 |
. . . 4
⊢ (𝜑 → (𝐺 DProd {〈∅, 𝑆〉}) = 𝑆) |
37 | 33, 36 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) = 𝑆) |
38 | | 1on 7454 |
. . . . . . . . . 10
⊢
1𝑜 ∈ On |
39 | 38 | elexi 3186 |
. . . . . . . . 9
⊢
1𝑜 ∈ V |
40 | 39 | prid2 4242 |
. . . . . . . 8
⊢
1𝑜 ∈ {∅,
1𝑜} |
41 | 40, 9 | eleqtrri 2687 |
. . . . . . 7
⊢
1𝑜 ∈ 2𝑜 |
42 | | fnressn 6330 |
. . . . . . 7
⊢ ((◡({𝑆} +𝑐 {𝑇}) Fn 2𝑜 ∧
1𝑜 ∈ 2𝑜) → (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}) =
{〈1𝑜, (◡({𝑆} +𝑐 {𝑇})‘1𝑜)〉}) |
43 | 22, 41, 42 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}) =
{〈1𝑜, (◡({𝑆} +𝑐 {𝑇})‘1𝑜)〉}) |
44 | | xpsc1 16044 |
. . . . . . . . 9
⊢ (𝑇 ∈ (SubGrp‘𝐺) → (◡({𝑆} +𝑐 {𝑇})‘1𝑜) = 𝑇) |
45 | 2, 44 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇})‘1𝑜) = 𝑇) |
46 | 45 | opeq2d 4347 |
. . . . . . 7
⊢ (𝜑 →
〈1𝑜, (◡({𝑆} +𝑐 {𝑇})‘1𝑜)〉 =
〈1𝑜, 𝑇〉) |
47 | 46 | sneqd 4137 |
. . . . . 6
⊢ (𝜑 →
{〈1𝑜, (◡({𝑆} +𝑐 {𝑇})‘1𝑜)〉} =
{〈1𝑜, 𝑇〉}) |
48 | 43, 47 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}) =
{〈1𝑜, 𝑇〉}) |
49 | 48 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜})) =
(𝐺 DProd
{〈1𝑜, 𝑇〉})) |
50 | | dprdsn 18258 |
. . . . . 6
⊢
((1𝑜 ∈ On ∧ 𝑇 ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈1𝑜,
𝑇〉} ∧ (𝐺 DProd
{〈1𝑜, 𝑇〉}) = 𝑇)) |
51 | 38, 2, 50 | sylancr 694 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈1𝑜,
𝑇〉} ∧ (𝐺 DProd
{〈1𝑜, 𝑇〉}) = 𝑇)) |
52 | 51 | simprd 478 |
. . . 4
⊢ (𝜑 → (𝐺 DProd {〈1𝑜, 𝑇〉}) = 𝑇) |
53 | 49, 52 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜})) = 𝑇) |
54 | 37, 53 | oveq12d 6567 |
. 2
⊢ (𝜑 → ((𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {∅})) ⊕ (𝐺 DProd (◡({𝑆} +𝑐 {𝑇}) ↾ {1𝑜}))) =
(𝑆 ⊕ 𝑇)) |
55 | 20, 54 | eqtrd 2644 |
1
⊢ (𝜑 → (𝐺 DProd ◡({𝑆} +𝑐 {𝑇})) = (𝑆 ⊕ 𝑇)) |