| Step | Hyp | Ref
| Expression |
| 1 | | imasmnd.u |
. . . 4
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
| 2 | | imasmnd.v |
. . . 4
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
| 3 | | imasmnd.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
| 4 | | imasmnd2.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑊) |
| 5 | 1, 2, 3, 4 | imasbas 17557 |
. . 3
⊢ (𝜑 → 𝐵 = (Base‘𝑈)) |
| 6 | | eqidd 2738 |
. . 3
⊢ (𝜑 → (+g‘𝑈) = (+g‘𝑈)) |
| 7 | | imasmnd.e |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) |
| 8 | | imasmnd.p |
. . . . 5
⊢ + =
(+g‘𝑅) |
| 9 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝑈) = (+g‘𝑈) |
| 10 | | imasmnd2.1 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉) |
| 11 | 10 | 3expb 1121 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉) |
| 12 | 11 | caovclg 7625 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) ∈ 𝑉) |
| 13 | 3, 7, 1, 2, 4, 8, 9, 12 | imasaddf 17578 |
. . . 4
⊢ (𝜑 → (+g‘𝑈):(𝐵 × 𝐵)⟶𝐵) |
| 14 | | fovcdm 7603 |
. . . 4
⊢
(((+g‘𝑈):(𝐵 × 𝐵)⟶𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+g‘𝑈)𝑣) ∈ 𝐵) |
| 15 | 13, 14 | syl3an1 1164 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+g‘𝑈)𝑣) ∈ 𝐵) |
| 16 | | forn 6823 |
. . . . . . . . . 10
⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵) |
| 17 | 3, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 = 𝐵) |
| 18 | 17 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ 𝑢 ∈ 𝐵)) |
| 19 | 17 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑣 ∈ ran 𝐹 ↔ 𝑣 ∈ 𝐵)) |
| 20 | 17 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ran 𝐹 ↔ 𝑤 ∈ 𝐵)) |
| 21 | 18, 19, 20 | 3anbi123d 1438 |
. . . . . . 7
⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) |
| 22 | | fofn 6822 |
. . . . . . . . 9
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉) |
| 23 | 3, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝑉) |
| 24 | | fvelrnb 6969 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑉 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢)) |
| 25 | | fvelrnb 6969 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑉 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣)) |
| 26 | | fvelrnb 6969 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑉 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)) |
| 27 | 24, 25, 26 | 3anbi123d 1438 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑉 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))) |
| 28 | 23, 27 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))) |
| 29 | 21, 28 | bitr3d 281 |
. . . . . 6
⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))) |
| 30 | | 3reeanv 3230 |
. . . . . 6
⊢
(∃𝑥 ∈
𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)) |
| 31 | 29, 30 | bitr4di 289 |
. . . . 5
⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤))) |
| 32 | | imasmnd2.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧)))) |
| 33 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝜑) |
| 34 | 10 | 3adant3r3 1185 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉) |
| 35 | | simpr3 1197 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ 𝑉) |
| 36 | 3, 7, 1, 2, 4, 8, 9 | imasaddval 17577 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 + 𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘(𝑥 + 𝑦))(+g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦) + 𝑧))) |
| 37 | 33, 34, 35, 36 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦) + 𝑧))) |
| 38 | | simpr1 1195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑥 ∈ 𝑉) |
| 39 | 12 | caovclg 7625 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉) |
| 40 | 39 | 3adantr1 1170 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉) |
| 41 | 3, 7, 1, 2, 4, 8, 9 | imasaddval 17577 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝑦 + 𝑧) ∈ 𝑉) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥 + (𝑦 + 𝑧)))) |
| 42 | 33, 38, 40, 41 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥 + (𝑦 + 𝑧)))) |
| 43 | 32, 37, 42 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘(𝑦 + 𝑧)))) |
| 44 | 3, 7, 1, 2, 4, 8, 9 | imasaddval 17577 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥 + 𝑦))) |
| 45 | 44 | 3adant3r3 1185 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥 + 𝑦))) |
| 46 | 45 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))(+g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘(𝑥 + 𝑦))(+g‘𝑈)(𝐹‘𝑧))) |
| 47 | 3, 7, 1, 2, 4, 8, 9 | imasaddval 17577 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦 + 𝑧))) |
| 48 | 47 | 3adant3r1 1183 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦 + 𝑧))) |
| 49 | 48 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+g‘𝑈)((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧))) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘(𝑦 + 𝑧)))) |
| 50 | 43, 46, 49 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))(+g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+g‘𝑈)((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧)))) |
| 51 | | simp1 1137 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑥) = 𝑢) |
| 52 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑦) = 𝑣) |
| 53 | 51, 52 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)) = (𝑢(+g‘𝑈)𝑣)) |
| 54 | | simp3 1139 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑧) = 𝑤) |
| 55 | 53, 54 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))(+g‘𝑈)(𝐹‘𝑧)) = ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤)) |
| 56 | 52, 54 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧)) = (𝑣(+g‘𝑈)𝑤)) |
| 57 | 51, 56 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+g‘𝑈)((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧))) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤))) |
| 58 | 55, 57 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))(+g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+g‘𝑈)((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧))) ↔ ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤)))) |
| 59 | 50, 58 | syl5ibcom 245 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤)))) |
| 60 | 59 | 3exp2 1355 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑉 → (𝑦 ∈ 𝑉 → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤))))))) |
| 61 | 60 | imp32 418 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤))))) |
| 62 | 61 | rexlimdv 3153 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤)))) |
| 63 | 62 | rexlimdvva 3213 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤)))) |
| 64 | 31, 63 | sylbid 240 |
. . . 4
⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤)))) |
| 65 | 64 | imp 406 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤))) |
| 66 | | fof 6820 |
. . . . 5
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵) |
| 67 | 3, 66 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:𝑉⟶𝐵) |
| 68 | | imasmnd2.3 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝑉) |
| 69 | 67, 68 | ffvelcdmd 7105 |
. . 3
⊢ (𝜑 → (𝐹‘ 0 ) ∈ 𝐵) |
| 70 | 23, 24 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢)) |
| 71 | 18, 70 | bitr3d 281 |
. . . . 5
⊢ (𝜑 → (𝑢 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢)) |
| 72 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝜑) |
| 73 | 68 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ∈ 𝑉) |
| 74 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
| 75 | 3, 7, 1, 2, 4, 8, 9 | imasaddval 17577 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0
)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 + 𝑥))) |
| 76 | 72, 73, 74, 75 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0
)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 + 𝑥))) |
| 77 | | imasmnd2.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥)) |
| 78 | 76, 77 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0
)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥)) |
| 79 | | oveq2 7439 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0
)(+g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘ 0
)(+g‘𝑈)𝑢)) |
| 80 | | id 22 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) = 𝑢 → (𝐹‘𝑥) = 𝑢) |
| 81 | 79, 80 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝐹‘𝑥) = 𝑢 → (((𝐹‘ 0
)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥) ↔ ((𝐹‘ 0
)(+g‘𝑈)𝑢) = 𝑢)) |
| 82 | 78, 81 | syl5ibcom 245 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0
)(+g‘𝑈)𝑢) = 𝑢)) |
| 83 | 82 | rexlimdva 3155 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0
)(+g‘𝑈)𝑢) = 𝑢)) |
| 84 | 71, 83 | sylbid 240 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ 𝐵 → ((𝐹‘ 0
)(+g‘𝑈)𝑢) = 𝑢)) |
| 85 | 84 | imp 406 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ((𝐹‘ 0
)(+g‘𝑈)𝑢) = 𝑢) |
| 86 | 3, 7, 1, 2, 4, 8, 9 | imasaddval 17577 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 0 ∈ 𝑉) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘ 0 )) = (𝐹‘(𝑥 + 0 ))) |
| 87 | 73, 86 | mpd3an3 1464 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘ 0 )) = (𝐹‘(𝑥 + 0 ))) |
| 88 | | imasmnd2.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑥 + 0 )) = (𝐹‘𝑥)) |
| 89 | 87, 88 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘ 0 )) = (𝐹‘𝑥)) |
| 90 | | oveq1 7438 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) = 𝑢 → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘ 0 )) = (𝑢(+g‘𝑈)(𝐹‘ 0 ))) |
| 91 | 90, 80 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝐹‘𝑥) = 𝑢 → (((𝐹‘𝑥)(+g‘𝑈)(𝐹‘ 0 )) = (𝐹‘𝑥) ↔ (𝑢(+g‘𝑈)(𝐹‘ 0 )) = 𝑢)) |
| 92 | 89, 91 | syl5ibcom 245 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → (𝑢(+g‘𝑈)(𝐹‘ 0 )) = 𝑢)) |
| 93 | 92 | rexlimdva 3155 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → (𝑢(+g‘𝑈)(𝐹‘ 0 )) = 𝑢)) |
| 94 | 71, 93 | sylbid 240 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ 𝐵 → (𝑢(+g‘𝑈)(𝐹‘ 0 )) = 𝑢)) |
| 95 | 94 | imp 406 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝑢(+g‘𝑈)(𝐹‘ 0 )) = 𝑢) |
| 96 | 5, 6, 15, 65, 69, 85, 95 | ismndd 18769 |
. 2
⊢ (𝜑 → 𝑈 ∈ Mnd) |
| 97 | 5, 6, 69, 85, 95 | grpidd 18684 |
. 2
⊢ (𝜑 → (𝐹‘ 0 ) =
(0g‘𝑈)) |
| 98 | 96, 97 | jca 511 |
1
⊢ (𝜑 → (𝑈 ∈ Mnd ∧ (𝐹‘ 0 ) =
(0g‘𝑈))) |