Step | Hyp | Ref
| Expression |
1 | | dprdsplit.1 |
. . 3
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
2 | | dprdsplit.2 |
. . . 4
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
3 | | fdm 5964 |
. . . 4
⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → dom 𝑆 = 𝐼) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝑆 = 𝐼) |
5 | | ssun1 3738 |
. . . . . . . 8
⊢ 𝐶 ⊆ (𝐶 ∪ 𝐷) |
6 | | dprdsplit.u |
. . . . . . . 8
⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷)) |
7 | 5, 6 | syl5sseqr 3617 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ⊆ 𝐼) |
8 | 1, 4, 7 | dprdres 18250 |
. . . . . 6
⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐶) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝐺 DProd 𝑆))) |
9 | 8 | simpld 474 |
. . . . 5
⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶)) |
10 | | dprdsubg 18246 |
. . . . 5
⊢ (𝐺dom DProd (𝑆 ↾ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺)) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺)) |
12 | | ssun2 3739 |
. . . . . . . 8
⊢ 𝐷 ⊆ (𝐶 ∪ 𝐷) |
13 | 12, 6 | syl5sseqr 3617 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ⊆ 𝐼) |
14 | 1, 4, 13 | dprdres 18250 |
. . . . . 6
⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐷) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑆))) |
15 | 14 | simpld 474 |
. . . . 5
⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷)) |
16 | | dprdsubg 18246 |
. . . . 5
⊢ (𝐺dom DProd (𝑆 ↾ 𝐷) → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
18 | | dprdsplit.i |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) |
19 | | eqid 2610 |
. . . . . . 7
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
20 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
21 | 2, 18, 6, 19, 20 | dmdprdsplit 18269 |
. . . . . 6
⊢ (𝜑 → (𝐺dom DProd 𝑆 ↔ ((𝐺dom DProd (𝑆 ↾ 𝐶) ∧ 𝐺dom DProd (𝑆 ↾ 𝐷)) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑆 ↾ 𝐷))) ∧ ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = {(0g‘𝐺)}))) |
22 | 1, 21 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ((𝐺dom DProd (𝑆 ↾ 𝐶) ∧ 𝐺dom DProd (𝑆 ↾ 𝐷)) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑆 ↾ 𝐷))) ∧ ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = {(0g‘𝐺)})) |
23 | 22 | simp2d 1067 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑆 ↾ 𝐷)))) |
24 | | dprdsplit.s |
. . . . 5
⊢ ⊕ =
(LSSum‘𝐺) |
25 | 24, 19 | lsmsubg 17892 |
. . . 4
⊢ (((𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑆 ↾ 𝐷)))) → ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺)) |
26 | 11, 17, 23, 25 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺)) |
27 | 6 | eleq2d 2673 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↔ 𝑥 ∈ (𝐶 ∪ 𝐷))) |
28 | | elun 3715 |
. . . . . 6
⊢ (𝑥 ∈ (𝐶 ∪ 𝐷) ↔ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷)) |
29 | 27, 28 | syl6bb 275 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↔ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷))) |
30 | 29 | biimpa 500 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷)) |
31 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐶 → ((𝑆 ↾ 𝐶)‘𝑥) = (𝑆‘𝑥)) |
32 | 31 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝑆 ↾ 𝐶)‘𝑥) = (𝑆‘𝑥)) |
33 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐺dom DProd (𝑆 ↾ 𝐶)) |
34 | 2, 7 | fssresd 5984 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ↾ 𝐶):𝐶⟶(SubGrp‘𝐺)) |
35 | | fdm 5964 |
. . . . . . . . . 10
⊢ ((𝑆 ↾ 𝐶):𝐶⟶(SubGrp‘𝐺) → dom (𝑆 ↾ 𝐶) = 𝐶) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑆 ↾ 𝐶) = 𝐶) |
37 | 36 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → dom (𝑆 ↾ 𝐶) = 𝐶) |
38 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) |
39 | 33, 37, 38 | dprdub 18247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝑆 ↾ 𝐶)‘𝑥) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) |
40 | 32, 39 | eqsstr3d 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) |
41 | 24 | lsmub1 17894 |
. . . . . . . 8
⊢ (((𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
42 | 11, 17, 41 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
43 | 42 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
44 | 40, 43 | sstrd 3578 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑆‘𝑥) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
45 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ((𝑆 ↾ 𝐷)‘𝑥) = (𝑆‘𝑥)) |
46 | 45 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑆 ↾ 𝐷)‘𝑥) = (𝑆‘𝑥)) |
47 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐺dom DProd (𝑆 ↾ 𝐷)) |
48 | 2, 13 | fssresd 5984 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) |
49 | | fdm 5964 |
. . . . . . . . . 10
⊢ ((𝑆 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺) → dom (𝑆 ↾ 𝐷) = 𝐷) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑆 ↾ 𝐷) = 𝐷) |
51 | 50 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → dom (𝑆 ↾ 𝐷) = 𝐷) |
52 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) |
53 | 47, 51, 52 | dprdub 18247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑆 ↾ 𝐷)‘𝑥) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷))) |
54 | 46, 53 | eqsstr3d 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷))) |
55 | 24 | lsmub2 17895 |
. . . . . . . 8
⊢ (((𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) → (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
56 | 11, 17, 55 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
57 | 56 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
58 | 54, 57 | sstrd 3578 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑆‘𝑥) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
59 | 44, 58 | jaodan 822 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷)) → (𝑆‘𝑥) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
60 | 30, 59 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆‘𝑥) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
61 | 1, 4, 26, 60 | dprdlub 18248 |
. 2
⊢ (𝜑 → (𝐺 DProd 𝑆) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |
62 | 8 | simprd 478 |
. . 3
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝐺 DProd 𝑆)) |
63 | 14 | simprd 478 |
. . 3
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑆)) |
64 | | dprdsubg 18246 |
. . . . 5
⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) |
65 | 1, 64 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) |
66 | 24 | lsmlub 17901 |
. . . 4
⊢ (((𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) → (((𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝐺 DProd 𝑆) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑆)) ↔ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ (𝐺 DProd 𝑆))) |
67 | 11, 17, 65, 66 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (((𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝐺 DProd 𝑆) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑆)) ↔ ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ (𝐺 DProd 𝑆))) |
68 | 62, 63, 67 | mpbi2and 958 |
. 2
⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ (𝐺 DProd 𝑆)) |
69 | 61, 68 | eqssd 3585 |
1
⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) |