| Step | Hyp | Ref
| Expression |
| 1 | | frmdplusg.p |
. . . 4
⊢ + =
(+g‘𝑀) |
| 2 | | frmdbas.m |
. . . . . 6
⊢ 𝑀 = (freeMnd‘𝐼) |
| 3 | | frmdbas.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
| 4 | 2, 3 | frmdbas 18865 |
. . . . . 6
⊢ (𝐼 ∈ V → 𝐵 = Word 𝐼) |
| 5 | | eqid 2737 |
. . . . . 6
⊢ ( ++
↾ (𝐵 × 𝐵)) = ( ++ ↾ (𝐵 × 𝐵)) |
| 6 | 2, 4, 5 | frmdval 18864 |
. . . . 5
⊢ (𝐼 ∈ V → 𝑀 = {〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), ( ++ ↾ (𝐵 × 𝐵))〉}) |
| 7 | 6 | fveq2d 6910 |
. . . 4
⊢ (𝐼 ∈ V →
(+g‘𝑀) =
(+g‘{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
++ ↾ (𝐵 × 𝐵))〉})) |
| 8 | 1, 7 | eqtrid 2789 |
. . 3
⊢ (𝐼 ∈ V → + =
(+g‘{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
++ ↾ (𝐵 × 𝐵))〉})) |
| 9 | | wrdexg 14562 |
. . . 4
⊢ (𝐼 ∈ V → Word 𝐼 ∈ V) |
| 10 | | ccatfn 14610 |
. . . . . . 7
⊢ ++ Fn (V
× V) |
| 11 | | xpss 5701 |
. . . . . . 7
⊢ (𝐵 × 𝐵) ⊆ (V × V) |
| 12 | | fnssres 6691 |
. . . . . . 7
⊢ (( ++ Fn
(V × V) ∧ (𝐵
× 𝐵) ⊆ (V
× V)) → ( ++ ↾ (𝐵 × 𝐵)) Fn (𝐵 × 𝐵)) |
| 13 | 10, 11, 12 | mp2an 692 |
. . . . . 6
⊢ ( ++
↾ (𝐵 × 𝐵)) Fn (𝐵 × 𝐵) |
| 14 | | ovres 7599 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥( ++ ↾ (𝐵 × 𝐵))𝑦) = (𝑥 ++ 𝑦)) |
| 15 | 2, 3 | frmdelbas 18866 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ Word 𝐼) |
| 16 | 2, 3 | frmdelbas 18866 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ Word 𝐼) |
| 17 | | ccatcl 14612 |
. . . . . . . . 9
⊢ ((𝑥 ∈ Word 𝐼 ∧ 𝑦 ∈ Word 𝐼) → (𝑥 ++ 𝑦) ∈ Word 𝐼) |
| 18 | 15, 16, 17 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ++ 𝑦) ∈ Word 𝐼) |
| 19 | 14, 18 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥( ++ ↾ (𝐵 × 𝐵))𝑦) ∈ Word 𝐼) |
| 20 | 19 | rgen2 3199 |
. . . . . 6
⊢
∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 (𝑥( ++ ↾ (𝐵 × 𝐵))𝑦) ∈ Word 𝐼 |
| 21 | | ffnov 7559 |
. . . . . 6
⊢ (( ++
↾ (𝐵 × 𝐵)):(𝐵 × 𝐵)⟶Word 𝐼 ↔ (( ++ ↾ (𝐵 × 𝐵)) Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥( ++ ↾ (𝐵 × 𝐵))𝑦) ∈ Word 𝐼)) |
| 22 | 13, 20, 21 | mpbir2an 711 |
. . . . 5
⊢ ( ++
↾ (𝐵 × 𝐵)):(𝐵 × 𝐵)⟶Word 𝐼 |
| 23 | 3 | fvexi 6920 |
. . . . . 6
⊢ 𝐵 ∈ V |
| 24 | 23, 23 | xpex 7773 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
| 25 | | fex2 7958 |
. . . . 5
⊢ ((( ++
↾ (𝐵 × 𝐵)):(𝐵 × 𝐵)⟶Word 𝐼 ∧ (𝐵 × 𝐵) ∈ V ∧ Word 𝐼 ∈ V) → ( ++ ↾ (𝐵 × 𝐵)) ∈ V) |
| 26 | 22, 24, 25 | mp3an12 1453 |
. . . 4
⊢ (Word
𝐼 ∈ V → ( ++
↾ (𝐵 × 𝐵)) ∈ V) |
| 27 | | eqid 2737 |
. . . . 5
⊢
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
++ ↾ (𝐵 × 𝐵))〉} =
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
++ ↾ (𝐵 × 𝐵))〉} |
| 28 | 27 | grpplusg 17332 |
. . . 4
⊢ (( ++
↾ (𝐵 × 𝐵)) ∈ V → ( ++ ↾
(𝐵 × 𝐵)) =
(+g‘{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
++ ↾ (𝐵 × 𝐵))〉})) |
| 29 | 9, 26, 28 | 3syl 18 |
. . 3
⊢ (𝐼 ∈ V → ( ++ ↾
(𝐵 × 𝐵)) =
(+g‘{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
++ ↾ (𝐵 × 𝐵))〉})) |
| 30 | 8, 29 | eqtr4d 2780 |
. 2
⊢ (𝐼 ∈ V → + = ( ++
↾ (𝐵 × 𝐵))) |
| 31 | | fvprc 6898 |
. . . . . . 7
⊢ (¬
𝐼 ∈ V →
(freeMnd‘𝐼) =
∅) |
| 32 | 2, 31 | eqtrid 2789 |
. . . . . 6
⊢ (¬
𝐼 ∈ V → 𝑀 = ∅) |
| 33 | 32 | fveq2d 6910 |
. . . . 5
⊢ (¬
𝐼 ∈ V →
(+g‘𝑀) =
(+g‘∅)) |
| 34 | 1, 33 | eqtrid 2789 |
. . . 4
⊢ (¬
𝐼 ∈ V → + =
(+g‘∅)) |
| 35 | | res0 6001 |
. . . . 5
⊢ ( ++
↾ ∅) = ∅ |
| 36 | | plusgid 17324 |
. . . . . 6
⊢
+g = Slot (+g‘ndx) |
| 37 | 36 | str0 17226 |
. . . . 5
⊢ ∅ =
(+g‘∅) |
| 38 | 35, 37 | eqtr2i 2766 |
. . . 4
⊢
(+g‘∅) = ( ++ ↾ ∅) |
| 39 | 34, 38 | eqtrdi 2793 |
. . 3
⊢ (¬
𝐼 ∈ V → + = ( ++
↾ ∅)) |
| 40 | 32 | fveq2d 6910 |
. . . . . . 7
⊢ (¬
𝐼 ∈ V →
(Base‘𝑀) =
(Base‘∅)) |
| 41 | | base0 17252 |
. . . . . . 7
⊢ ∅ =
(Base‘∅) |
| 42 | 40, 3, 41 | 3eqtr4g 2802 |
. . . . . 6
⊢ (¬
𝐼 ∈ V → 𝐵 = ∅) |
| 43 | 42 | xpeq2d 5715 |
. . . . 5
⊢ (¬
𝐼 ∈ V → (𝐵 × 𝐵) = (𝐵 × ∅)) |
| 44 | | xp0 6178 |
. . . . 5
⊢ (𝐵 × ∅) =
∅ |
| 45 | 43, 44 | eqtrdi 2793 |
. . . 4
⊢ (¬
𝐼 ∈ V → (𝐵 × 𝐵) = ∅) |
| 46 | 45 | reseq2d 5997 |
. . 3
⊢ (¬
𝐼 ∈ V → ( ++
↾ (𝐵 × 𝐵)) = ( ++ ↾
∅)) |
| 47 | 39, 46 | eqtr4d 2780 |
. 2
⊢ (¬
𝐼 ∈ V → + = ( ++
↾ (𝐵 × 𝐵))) |
| 48 | 30, 47 | pm2.61i 182 |
1
⊢ + = ( ++
↾ (𝐵 × 𝐵)) |