| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . 3
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ 𝑊) | 
| 2 |  | simpr 484 | . . 3
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ 𝑊) | 
| 3 |  | frgpadd.w | . . . . . . . 8
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) | 
| 4 | 3 | efgrcl 19734 | . . . . . . 7
⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) | 
| 5 | 4 | adantr 480 | . . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) | 
| 6 | 5 | simpld 494 | . . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐼 ∈ V) | 
| 7 |  | frgpadd.g | . . . . . 6
⊢ 𝐺 = (freeGrp‘𝐼) | 
| 8 |  | eqid 2736 | . . . . . 6
⊢
(freeMnd‘(𝐼
× 2o)) = (freeMnd‘(𝐼 × 2o)) | 
| 9 |  | frgpadd.r | . . . . . 6
⊢  ∼ = (
~FG ‘𝐼) | 
| 10 | 7, 8, 9 | frgpval 19777 | . . . . 5
⊢ (𝐼 ∈ V → 𝐺 = ((freeMnd‘(𝐼 × 2o))
/s ∼ )) | 
| 11 | 6, 10 | syl 17 | . . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐺 = ((freeMnd‘(𝐼 × 2o))
/s ∼ )) | 
| 12 | 5 | simprd 495 | . . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝑊 = Word (𝐼 × 2o)) | 
| 13 |  | 2on 8521 | . . . . . . 7
⊢
2o ∈ On | 
| 14 |  | xpexg 7771 | . . . . . . 7
⊢ ((𝐼 ∈ V ∧ 2o
∈ On) → (𝐼
× 2o) ∈ V) | 
| 15 | 6, 13, 14 | sylancl 586 | . . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝐼 × 2o) ∈
V) | 
| 16 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘(freeMnd‘(𝐼 × 2o))) =
(Base‘(freeMnd‘(𝐼 × 2o))) | 
| 17 | 8, 16 | frmdbas 18866 | . . . . . 6
⊢ ((𝐼 × 2o) ∈ V
→ (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 ×
2o)) | 
| 18 | 15, 17 | syl 17 | . . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (Base‘(freeMnd‘(𝐼 × 2o))) = Word
(𝐼 ×
2o)) | 
| 19 | 12, 18 | eqtr4d 2779 | . . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝑊 = (Base‘(freeMnd‘(𝐼 ×
2o)))) | 
| 20 | 3, 9 | efger 19737 | . . . . 5
⊢  ∼ Er
𝑊 | 
| 21 | 20 | a1i 11 | . . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∼ Er 𝑊) | 
| 22 | 8 | frmdmnd 18873 | . . . . 5
⊢ ((𝐼 × 2o) ∈ V
→ (freeMnd‘(𝐼
× 2o)) ∈ Mnd) | 
| 23 | 15, 22 | syl 17 | . . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (freeMnd‘(𝐼 × 2o)) ∈
Mnd) | 
| 24 |  | eqid 2736 | . . . . . 6
⊢
(+g‘(freeMnd‘(𝐼 × 2o))) =
(+g‘(freeMnd‘(𝐼 × 2o))) | 
| 25 | 7, 8, 9, 24 | frgpcpbl 19778 | . . . . 5
⊢ ((𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑) → (𝑎(+g‘(freeMnd‘(𝐼 × 2o)))𝑐) ∼ (𝑏(+g‘(freeMnd‘(𝐼 × 2o)))𝑑)) | 
| 26 | 25 | a1i 11 | . . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ((𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑) → (𝑎(+g‘(freeMnd‘(𝐼 × 2o)))𝑐) ∼ (𝑏(+g‘(freeMnd‘(𝐼 × 2o)))𝑑))) | 
| 27 | 23 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → (freeMnd‘(𝐼 × 2o)) ∈
Mnd) | 
| 28 |  | simprl 770 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → 𝑏 ∈ 𝑊) | 
| 29 | 19 | adantr 480 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → 𝑊 = (Base‘(freeMnd‘(𝐼 ×
2o)))) | 
| 30 | 28, 29 | eleqtrd 2842 | . . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → 𝑏 ∈ (Base‘(freeMnd‘(𝐼 ×
2o)))) | 
| 31 |  | simprr 772 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → 𝑑 ∈ 𝑊) | 
| 32 | 31, 29 | eleqtrd 2842 | . . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → 𝑑 ∈ (Base‘(freeMnd‘(𝐼 ×
2o)))) | 
| 33 | 16, 24 | mndcl 18756 | . . . . . 6
⊢
(((freeMnd‘(𝐼
× 2o)) ∈ Mnd ∧ 𝑏 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ∧
𝑑 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) → (𝑏(+g‘(freeMnd‘(𝐼 × 2o)))𝑑) ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) | 
| 34 | 27, 30, 32, 33 | syl3anc 1372 | . . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → (𝑏(+g‘(freeMnd‘(𝐼 × 2o)))𝑑) ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) | 
| 35 | 34, 29 | eleqtrrd 2843 | . . . 4
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → (𝑏(+g‘(freeMnd‘(𝐼 × 2o)))𝑑) ∈ 𝑊) | 
| 36 |  | frgpadd.n | . . . 4
⊢  + =
(+g‘𝐺) | 
| 37 | 11, 19, 21, 23, 26, 35, 24, 36 | qusaddval 17599 | . . 3
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ([𝐴] ∼ + [𝐵] ∼ ) = [(𝐴(+g‘(freeMnd‘(𝐼 × 2o)))𝐵)] ∼ ) | 
| 38 | 1, 2, 37 | mpd3an23 1464 | . 2
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ([𝐴] ∼ + [𝐵] ∼ ) = [(𝐴(+g‘(freeMnd‘(𝐼 × 2o)))𝐵)] ∼ ) | 
| 39 | 1, 19 | eleqtrd 2842 | . . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ (Base‘(freeMnd‘(𝐼 ×
2o)))) | 
| 40 | 2, 19 | eleqtrd 2842 | . . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ (Base‘(freeMnd‘(𝐼 ×
2o)))) | 
| 41 | 8, 16, 24 | frmdadd 18869 | . . . 4
⊢ ((𝐴 ∈
(Base‘(freeMnd‘(𝐼 × 2o))) ∧ 𝐵 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) → (𝐴(+g‘(freeMnd‘(𝐼 × 2o)))𝐵) = (𝐴 ++ 𝐵)) | 
| 42 | 39, 40, 41 | syl2anc 584 | . . 3
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝐴(+g‘(freeMnd‘(𝐼 × 2o)))𝐵) = (𝐴 ++ 𝐵)) | 
| 43 | 42 | eceq1d 8786 | . 2
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → [(𝐴(+g‘(freeMnd‘(𝐼 × 2o)))𝐵)] ∼ = [(𝐴 ++ 𝐵)] ∼ ) | 
| 44 | 38, 43 | eqtrd 2776 | 1
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ([𝐴] ∼ + [𝐵] ∼ ) = [(𝐴 ++ 𝐵)] ∼ ) |