Step |
Hyp |
Ref |
Expression |
1 |
|
eldprdi.0 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
2 |
|
eldprdi.w |
⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 } |
3 |
|
eldprdi.1 |
⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 ) |
4 |
|
eldprdi.2 |
⊢ ( 𝜑 → dom 𝑆 = 𝐼 ) |
5 |
|
dprdfid.3 |
⊢ ( 𝜑 → 𝑋 ∈ 𝐼 ) |
6 |
|
dprdfid.4 |
⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 ‘ 𝑋 ) ) |
7 |
|
dprdfid.f |
⊢ 𝐹 = ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) |
8 |
6
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ 𝑛 = 𝑋 ) → 𝐴 ∈ ( 𝑆 ‘ 𝑋 ) ) |
9 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ 𝑛 = 𝑋 ) → 𝑛 = 𝑋 ) |
10 |
9
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ 𝑛 = 𝑋 ) → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ 𝑋 ) ) |
11 |
8 10
|
eleqtrrd |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ 𝑛 = 𝑋 ) → 𝐴 ∈ ( 𝑆 ‘ 𝑛 ) ) |
12 |
3 4
|
dprdf2 |
⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ) |
13 |
12
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑛 ) ∈ ( SubGrp ‘ 𝐺 ) ) |
14 |
1
|
subg0cl |
⊢ ( ( 𝑆 ‘ 𝑛 ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( 𝑆 ‘ 𝑛 ) ) |
15 |
13 14
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 0 ∈ ( 𝑆 ‘ 𝑛 ) ) |
16 |
15
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ¬ 𝑛 = 𝑋 ) → 0 ∈ ( 𝑆 ‘ 𝑛 ) ) |
17 |
11 16
|
ifclda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ∈ ( 𝑆 ‘ 𝑛 ) ) |
18 |
3 4
|
dprddomcld |
⊢ ( 𝜑 → 𝐼 ∈ V ) |
19 |
1
|
fvexi |
⊢ 0 ∈ V |
20 |
19
|
a1i |
⊢ ( 𝜑 → 0 ∈ V ) |
21 |
|
eqid |
⊢ ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) = ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) |
22 |
18 20 21
|
sniffsupp |
⊢ ( 𝜑 → ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) finSupp 0 ) |
23 |
2 3 4 17 22
|
dprdwd |
⊢ ( 𝜑 → ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) ∈ 𝑊 ) |
24 |
7 23
|
eqeltrid |
⊢ ( 𝜑 → 𝐹 ∈ 𝑊 ) |
25 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
26 |
|
dprdgrp |
⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp ) |
27 |
|
grpmnd |
⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd ) |
28 |
3 26 27
|
3syl |
⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
29 |
2 3 4 24 25
|
dprdff |
⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) ) |
30 |
7
|
oveq1i |
⊢ ( 𝐹 supp 0 ) = ( ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) supp 0 ) |
31 |
|
eldifsni |
⊢ ( 𝑛 ∈ ( 𝐼 ∖ { 𝑋 } ) → 𝑛 ≠ 𝑋 ) |
32 |
31
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐼 ∖ { 𝑋 } ) ) → 𝑛 ≠ 𝑋 ) |
33 |
|
ifnefalse |
⊢ ( 𝑛 ≠ 𝑋 → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) = 0 ) |
34 |
32 33
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐼 ∖ { 𝑋 } ) ) → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) = 0 ) |
35 |
34 18
|
suppss2 |
⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) supp 0 ) ⊆ { 𝑋 } ) |
36 |
30 35
|
eqsstrid |
⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ { 𝑋 } ) |
37 |
25 1 28 18 5 29 36
|
gsumpt |
⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐹 ‘ 𝑋 ) ) |
38 |
|
iftrue |
⊢ ( 𝑛 = 𝑋 → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) = 𝐴 ) |
39 |
7 38 5 6
|
fvmptd3 |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝐴 ) |
40 |
37 39
|
eqtrd |
⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = 𝐴 ) |
41 |
24 40
|
jca |
⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ∧ ( 𝐺 Σg 𝐹 ) = 𝐴 ) ) |