Step |
Hyp |
Ref |
Expression |
1 |
|
frmdmnd.m |
⊢ 𝑀 = ( freeMnd ‘ 𝐼 ) |
2 |
|
eqid |
⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) |
3 |
|
eqid |
⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 ) |
4 |
|
eqid |
⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 ) |
5 |
|
wrd0 |
⊢ ∅ ∈ Word 𝐼 |
6 |
1 2
|
frmdbas |
⊢ ( 𝐼 ∈ V → ( Base ‘ 𝑀 ) = Word 𝐼 ) |
7 |
5 6
|
eleqtrrid |
⊢ ( 𝐼 ∈ V → ∅ ∈ ( Base ‘ 𝑀 ) ) |
8 |
1 2 4
|
frmdadd |
⊢ ( ( ∅ ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ( +g ‘ 𝑀 ) 𝑥 ) = ( ∅ ++ 𝑥 ) ) |
9 |
7 8
|
sylan |
⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ( +g ‘ 𝑀 ) 𝑥 ) = ( ∅ ++ 𝑥 ) ) |
10 |
1 2
|
frmdelbas |
⊢ ( 𝑥 ∈ ( Base ‘ 𝑀 ) → 𝑥 ∈ Word 𝐼 ) |
11 |
10
|
adantl |
⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → 𝑥 ∈ Word 𝐼 ) |
12 |
|
ccatlid |
⊢ ( 𝑥 ∈ Word 𝐼 → ( ∅ ++ 𝑥 ) = 𝑥 ) |
13 |
11 12
|
syl |
⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ++ 𝑥 ) = 𝑥 ) |
14 |
9 13
|
eqtrd |
⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ( +g ‘ 𝑀 ) 𝑥 ) = 𝑥 ) |
15 |
1 2 4
|
frmdadd |
⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ ∅ ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ∅ ) = ( 𝑥 ++ ∅ ) ) |
16 |
15
|
ancoms |
⊢ ( ( ∅ ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ∅ ) = ( 𝑥 ++ ∅ ) ) |
17 |
7 16
|
sylan |
⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ∅ ) = ( 𝑥 ++ ∅ ) ) |
18 |
|
ccatrid |
⊢ ( 𝑥 ∈ Word 𝐼 → ( 𝑥 ++ ∅ ) = 𝑥 ) |
19 |
11 18
|
syl |
⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ++ ∅ ) = 𝑥 ) |
20 |
17 19
|
eqtrd |
⊢ ( ( 𝐼 ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ∅ ) = 𝑥 ) |
21 |
2 3 4 7 14 20
|
ismgmid2 |
⊢ ( 𝐼 ∈ V → ∅ = ( 0g ‘ 𝑀 ) ) |
22 |
|
0g0 |
⊢ ∅ = ( 0g ‘ ∅ ) |
23 |
|
fvprc |
⊢ ( ¬ 𝐼 ∈ V → ( freeMnd ‘ 𝐼 ) = ∅ ) |
24 |
1 23
|
syl5eq |
⊢ ( ¬ 𝐼 ∈ V → 𝑀 = ∅ ) |
25 |
24
|
fveq2d |
⊢ ( ¬ 𝐼 ∈ V → ( 0g ‘ 𝑀 ) = ( 0g ‘ ∅ ) ) |
26 |
22 25
|
eqtr4id |
⊢ ( ¬ 𝐼 ∈ V → ∅ = ( 0g ‘ 𝑀 ) ) |
27 |
21 26
|
pm2.61i |
⊢ ∅ = ( 0g ‘ 𝑀 ) |