Step | Hyp | Ref
| Expression |
1 | | eldprdi.w |
. . . . . . 7
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } |
2 | | eldprdi.1 |
. . . . . . 7
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
3 | | eldprdi.2 |
. . . . . . 7
⊢ (𝜑 → dom 𝑆 = 𝐼) |
4 | | eldprdi.3 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ 𝑊) |
5 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | 1, 2, 3, 4, 5 | dprdff 18234 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐼⟶(Base‘𝐺)) |
7 | 6 | feqmptd 6159 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥))) |
8 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥))) |
9 | 1, 2, 3, 4 | dprdfcl 18235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ (𝑆‘𝑥)) |
10 | 9 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ (𝑆‘𝑥)) |
11 | | eldprdi.0 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝐺) |
12 | 2 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 𝐺dom DProd 𝑆) |
13 | 3 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → dom 𝑆 = 𝐼) |
14 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
15 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 )) = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 )) |
16 | 11, 1, 12, 13, 14, 10, 15 | dprdfid 18239 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 )) ∈ 𝑊 ∧ (𝐺 Σg (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ))) = (𝐹‘𝑥))) |
17 | 16 | simpld 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 )) ∈ 𝑊) |
18 | 4 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ 𝑊) |
19 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(-g‘𝐺) = (-g‘𝐺) |
20 | 11, 1, 12, 13, 17, 18, 19 | dprdfsub 18243 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ))
∘𝑓 (-g‘𝐺)𝐹) ∈ 𝑊 ∧ (𝐺 Σg ((𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ))
∘𝑓 (-g‘𝐺)𝐹)) = ((𝐺 Σg (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)))(-g‘𝐺)(𝐺 Σg 𝐹)))) |
21 | 20 | simprd 478 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐺 Σg ((𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ))
∘𝑓 (-g‘𝐺)𝐹)) = ((𝐺 Σg (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)))(-g‘𝐺)(𝐺 Σg 𝐹))) |
22 | 2, 3 | dprddomcld 18223 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ V) |
23 | 22 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ V) |
24 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘𝑥) ∈ V |
25 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) ∈ V |
26 | 11, 25 | eqeltri 2684 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
27 | 24, 26 | ifex 4106 |
. . . . . . . . . . . . 13
⊢ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ) ∈
V |
28 | 27 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) → if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ) ∈
V) |
29 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐹‘𝑦) ∈ V |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ V) |
31 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 )) = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ))) |
32 | 6 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 𝐹:𝐼⟶(Base‘𝐺)) |
33 | 32 | feqmptd 6159 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 𝐹 = (𝑦 ∈ 𝐼 ↦ (𝐹‘𝑦))) |
34 | 23, 28, 30, 31, 33 | offval2 6812 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ))
∘𝑓 (-g‘𝐺)𝐹) = (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦)))) |
35 | 34 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐺 Σg ((𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ))
∘𝑓 (-g‘𝐺)𝐹)) = (𝐺 Σg (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦))))) |
36 | 16 | simprd 478 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐺 Σg (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ))) = (𝐹‘𝑥)) |
37 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐺 Σg 𝐹) = 0 ) |
38 | 36, 37 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((𝐺 Σg (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)))(-g‘𝐺)(𝐺 Σg 𝐹)) = ((𝐹‘𝑥)(-g‘𝐺) 0 )) |
39 | | dprdgrp 18227 |
. . . . . . . . . . . . 13
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
40 | 12, 39 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 𝐺 ∈ Grp) |
41 | 32, 14 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ (Base‘𝐺)) |
42 | 5, 11, 19 | grpsubid1 17323 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝐹‘𝑥) ∈ (Base‘𝐺)) → ((𝐹‘𝑥)(-g‘𝐺) 0 ) = (𝐹‘𝑥)) |
43 | 40, 41, 42 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((𝐹‘𝑥)(-g‘𝐺) 0 ) = (𝐹‘𝑥)) |
44 | 38, 43 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((𝐺 Σg (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)))(-g‘𝐺)(𝐺 Σg 𝐹)) = (𝐹‘𝑥)) |
45 | 21, 35, 44 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐺 Σg (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦)))) = (𝐹‘𝑥)) |
46 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
47 | | grpmnd 17252 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
48 | 2, 39, 47 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ Mnd) |
49 | 48 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 𝐺 ∈ Mnd) |
50 | 5 | subgacs 17452 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
51 | | acsmre 16136 |
. . . . . . . . . . . . 13
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
52 | 40, 50, 51 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
53 | | imassrn 5396 |
. . . . . . . . . . . . . 14
⊢ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ ran 𝑆 |
54 | 2, 3 | dprdf2 18229 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
55 | 54 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
56 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
58 | | mresspw 16075 |
. . . . . . . . . . . . . . . 16
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
59 | 52, 58 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
60 | 57, 59 | sstrd 3578 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺)) |
61 | 53, 60 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺)) |
62 | | sspwuni 4547 |
. . . . . . . . . . . . 13
⊢ ((𝑆 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
63 | 61, 62 | sylib 207 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ∪ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
64 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺)) |
65 | 64 | mrccl 16094 |
. . . . . . . . . . . 12
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
66 | 52, 63, 65 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
67 | | subgsubm 17439 |
. . . . . . . . . . 11
⊢
(((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ∈ (SubMnd‘𝐺)) |
68 | 66, 67 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ∈ (SubMnd‘𝐺)) |
69 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) = if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ) → ((𝐹‘𝑥)(-g‘𝐺)(𝐹‘𝑦)) = (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦))) |
70 | 69 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑥) = if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ) → (((𝐹‘𝑥)(-g‘𝐺)(𝐹‘𝑦)) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ↔ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦)) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))))) |
71 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ ( 0 = if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ) → ( 0
(-g‘𝐺)(𝐹‘𝑦)) = (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦))) |
72 | 71 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ( 0 = if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ) → (( 0
(-g‘𝐺)(𝐹‘𝑦)) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ↔ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦)) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))))) |
73 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
74 | 73 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥)) |
75 | 74 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ 𝑦 = 𝑥) → ((𝐹‘𝑥)(-g‘𝐺)(𝐹‘𝑦)) = ((𝐹‘𝑥)(-g‘𝐺)(𝐹‘𝑥))) |
76 | 5, 11, 19 | grpsubid 17322 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ (𝐹‘𝑥) ∈ (Base‘𝐺)) → ((𝐹‘𝑥)(-g‘𝐺)(𝐹‘𝑥)) = 0 ) |
77 | 40, 41, 76 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((𝐹‘𝑥)(-g‘𝐺)(𝐹‘𝑥)) = 0 ) |
78 | 11 | subg0cl 17425 |
. . . . . . . . . . . . . . . 16
⊢
(((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → 0 ∈
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) |
79 | 66, 78 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 0 ∈
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) |
80 | 77, 79 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((𝐹‘𝑥)(-g‘𝐺)(𝐹‘𝑥)) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
81 | 80 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ 𝑦 = 𝑥) → ((𝐹‘𝑥)(-g‘𝐺)(𝐹‘𝑥)) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
82 | 75, 81 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ 𝑦 = 𝑥) → ((𝐹‘𝑥)(-g‘𝐺)(𝐹‘𝑦)) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
83 | 66 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
84 | 83, 78 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → 0 ∈
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) |
85 | 52, 64, 63 | mrcssidd 16108 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ∪ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
86 | 85 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → ∪ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
87 | 1, 12, 13, 18 | dprdfcl 18235 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (𝑆‘𝑦)) |
88 | 87 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → (𝐹‘𝑦) ∈ (𝑆‘𝑦)) |
89 | | ffn 5958 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → 𝑆 Fn 𝐼) |
90 | 55, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑆 Fn 𝐼) |
91 | 90 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → 𝑆 Fn 𝐼) |
92 | | difssd 3700 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → (𝐼 ∖ {𝑥}) ⊆ 𝐼) |
93 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ≠ 𝑥 ↔ ¬ 𝑦 = 𝑥) |
94 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝐼 ∖ {𝑥}) ↔ (𝑦 ∈ 𝐼 ∧ 𝑦 ≠ 𝑥)) |
95 | 94 | biimpri 217 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑦 ≠ 𝑥) → 𝑦 ∈ (𝐼 ∖ {𝑥})) |
96 | 93, 95 | sylan2br 492 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐼 ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ (𝐼 ∖ {𝑥})) |
97 | 96 | adantll 746 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ (𝐼 ∖ {𝑥})) |
98 | | fnfvima 6400 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 Fn 𝐼 ∧ (𝐼 ∖ {𝑥}) ⊆ 𝐼 ∧ 𝑦 ∈ (𝐼 ∖ {𝑥})) → (𝑆‘𝑦) ∈ (𝑆 “ (𝐼 ∖ {𝑥}))) |
99 | 91, 92, 97, 98 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → (𝑆‘𝑦) ∈ (𝑆 “ (𝐼 ∖ {𝑥}))) |
100 | | elunii 4377 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑦) ∈ (𝑆‘𝑦) ∧ (𝑆‘𝑦) ∈ (𝑆 “ (𝐼 ∖ {𝑥}))) → (𝐹‘𝑦) ∈ ∪ (𝑆 “ (𝐼 ∖ {𝑥}))) |
101 | 88, 99, 100 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → (𝐹‘𝑦) ∈ ∪ (𝑆 “ (𝐼 ∖ {𝑥}))) |
102 | 86, 101 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → (𝐹‘𝑦) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
103 | 19 | subgsubcl 17428 |
. . . . . . . . . . . . 13
⊢
((((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ 0 ∈
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))) ∧ (𝐹‘𝑦) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) → ( 0
(-g‘𝐺)(𝐹‘𝑦)) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
104 | 83, 84, 102, 103 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝐺 Σg
𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) ∧ ¬ 𝑦 = 𝑥) → ( 0 (-g‘𝐺)(𝐹‘𝑦)) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
105 | 70, 72, 82, 104 | ifbothda 4073 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) → (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦)) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
106 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦))) |
107 | 105, 106 | fmptd 6292 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦))):𝐼⟶((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
108 | 20 | simpld 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, (𝐹‘𝑥), 0 ))
∘𝑓 (-g‘𝐺)𝐹) ∈ 𝑊) |
109 | 34, 108 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦))) ∈ 𝑊) |
110 | 1, 12, 13, 109, 46 | dprdfcntz 18237 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ran (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦))) ⊆ ((Cntz‘𝐺)‘ran (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦))))) |
111 | 1, 12, 13, 109 | dprdffsupp 18236 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦))) finSupp 0 ) |
112 | 11, 46, 49, 23, 68, 107, 110, 111 | gsumzsubmcl 18141 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐺 Σg (𝑦 ∈ 𝐼 ↦ (if(𝑦 = 𝑥, (𝐹‘𝑥), 0
)(-g‘𝐺)(𝐹‘𝑦)))) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
113 | 45, 112 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) |
114 | 10, 113 | elind 3760 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))))) |
115 | 12, 13, 14, 11, 64 | dprddisj 18231 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) = { 0 }) |
116 | 114, 115 | eleqtrd 2690 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ { 0 }) |
117 | | elsni 4142 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ { 0 } → (𝐹‘𝑥) = 0 ) |
118 | 116, 117 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) = 0 ) |
119 | 118 | mpteq2dva 4672 |
. . . 4
⊢ ((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐼 ↦ 0 )) |
120 | 8, 119 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ (𝐺 Σg 𝐹) = 0 ) → 𝐹 = (𝑥 ∈ 𝐼 ↦ 0 )) |
121 | 120 | ex 449 |
. 2
⊢ (𝜑 → ((𝐺 Σg 𝐹) = 0 → 𝐹 = (𝑥 ∈ 𝐼 ↦ 0 ))) |
122 | 11 | gsumz 17197 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝐼 ∈ V) → (𝐺 Σg
(𝑥 ∈ 𝐼 ↦ 0 )) = 0 ) |
123 | 48, 22, 122 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐼 ↦ 0 )) = 0 ) |
124 | | oveq2 6557 |
. . . 4
⊢ (𝐹 = (𝑥 ∈ 𝐼 ↦ 0 ) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝑥 ∈ 𝐼 ↦ 0 ))) |
125 | 124 | eqeq1d 2612 |
. . 3
⊢ (𝐹 = (𝑥 ∈ 𝐼 ↦ 0 ) → ((𝐺 Σg
𝐹) = 0 ↔ (𝐺 Σg (𝑥 ∈ 𝐼 ↦ 0 )) = 0 )) |
126 | 123, 125 | syl5ibrcom 236 |
. 2
⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐼 ↦ 0 ) → (𝐺 Σg
𝐹) = 0 )) |
127 | 121, 126 | impbid 201 |
1
⊢ (𝜑 → ((𝐺 Σg 𝐹) = 0 ↔ 𝐹 = (𝑥 ∈ 𝐼 ↦ 0 ))) |