| Step | Hyp | Ref
| Expression |
| 1 | | pwssplit4.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ↾ 𝐵)) |
| 2 | | pwssplit4.k |
. . . . . 6
⊢ 𝐾 = {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (𝐴 × { 0 })} |
| 3 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (𝐴 × { 0 })} ⊆ 𝐺 |
| 4 | 2, 3 | eqsstri 4030 |
. . . . 5
⊢ 𝐾 ⊆ 𝐺 |
| 5 | | resmpt 6055 |
. . . . 5
⊢ (𝐾 ⊆ 𝐺 → ((𝑥 ∈ 𝐺 ↦ (𝑥 ↾ 𝐵)) ↾ 𝐾) = (𝑥 ∈ 𝐾 ↦ (𝑥 ↾ 𝐵))) |
| 6 | 4, 5 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ 𝐺 ↦ (𝑥 ↾ 𝐵)) ↾ 𝐾) = (𝑥 ∈ 𝐾 ↦ (𝑥 ↾ 𝐵)) |
| 7 | 1, 6 | eqtr4i 2768 |
. . 3
⊢ 𝐹 = ((𝑥 ∈ 𝐺 ↦ (𝑥 ↾ 𝐵)) ↾ 𝐾) |
| 8 | | ssun2 4179 |
. . . . . 6
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
| 9 | 8 | a1i 11 |
. . . . 5
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ⊆ (𝐴 ∪ 𝐵)) |
| 10 | | pwssplit4.e |
. . . . . 6
⊢ 𝐸 = (𝑅 ↑s (𝐴 ∪ 𝐵)) |
| 11 | | pwssplit4.d |
. . . . . 6
⊢ 𝐷 = (𝑅 ↑s 𝐵) |
| 12 | | pwssplit4.g |
. . . . . 6
⊢ 𝐺 = (Base‘𝐸) |
| 13 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 14 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐺 ↦ (𝑥 ↾ 𝐵)) = (𝑥 ∈ 𝐺 ↦ (𝑥 ↾ 𝐵)) |
| 15 | 10, 11, 12, 13, 14 | pwssplit3 21060 |
. . . . 5
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ 𝐵 ⊆ (𝐴 ∪ 𝐵)) → (𝑥 ∈ 𝐺 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐸 LMHom 𝐷)) |
| 16 | 9, 15 | syld3an3 1411 |
. . . 4
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑥 ∈ 𝐺 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐸 LMHom 𝐷)) |
| 17 | | simp1 1137 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝑅 ∈ LMod) |
| 18 | | lmodgrp 20865 |
. . . . . . . . . 10
⊢ (𝑅 ∈ LMod → 𝑅 ∈ Grp) |
| 19 | | grpmnd 18958 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Grp → 𝑅 ∈ Mnd) |
| 20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝑅 ∈ Mnd) |
| 21 | | ssun1 4178 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
| 22 | | ssexg 5323 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ∈ 𝑉) → 𝐴 ∈ V) |
| 23 | 21, 22 | mpan 690 |
. . . . . . . . . 10
⊢ ((𝐴 ∪ 𝐵) ∈ 𝑉 → 𝐴 ∈ V) |
| 24 | 23 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ∈ V) |
| 25 | | pwssplit4.c |
. . . . . . . . . 10
⊢ 𝐶 = (𝑅 ↑s 𝐴) |
| 26 | | pwssplit4.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑅) |
| 27 | 25, 26 | pws0g 18786 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ 𝐴 ∈ V) → (𝐴 × { 0 }) =
(0g‘𝐶)) |
| 28 | 20, 24, 27 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 × { 0 }) =
(0g‘𝐶)) |
| 29 | 28 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑦 ↾ 𝐴) = (𝐴 × { 0 }) ↔ (𝑦 ↾ 𝐴) = (0g‘𝐶))) |
| 30 | 29 | rabbidv 3444 |
. . . . . 6
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (𝐴 × { 0 })} = {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (0g‘𝐶)}) |
| 31 | 2, 30 | eqtrid 2789 |
. . . . 5
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐾 = {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (0g‘𝐶)}) |
| 32 | 21 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ⊆ (𝐴 ∪ 𝐵)) |
| 33 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 34 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐺 ↦ (𝑦 ↾ 𝐴)) = (𝑦 ∈ 𝐺 ↦ (𝑦 ↾ 𝐴)) |
| 35 | 10, 25, 12, 33, 34 | pwssplit3 21060 |
. . . . . . 7
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ 𝐴 ⊆ (𝐴 ∪ 𝐵)) → (𝑦 ∈ 𝐺 ↦ (𝑦 ↾ 𝐴)) ∈ (𝐸 LMHom 𝐶)) |
| 36 | 32, 35 | syld3an3 1411 |
. . . . . 6
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑦 ∈ 𝐺 ↦ (𝑦 ↾ 𝐴)) ∈ (𝐸 LMHom 𝐶)) |
| 37 | | fvex 6919 |
. . . . . . . . 9
⊢
(0g‘𝐶) ∈ V |
| 38 | 34 | mptiniseg 6259 |
. . . . . . . . 9
⊢
((0g‘𝐶) ∈ V → (◡(𝑦 ∈ 𝐺 ↦ (𝑦 ↾ 𝐴)) “ {(0g‘𝐶)}) = {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (0g‘𝐶)}) |
| 39 | 37, 38 | ax-mp 5 |
. . . . . . . 8
⊢ (◡(𝑦 ∈ 𝐺 ↦ (𝑦 ↾ 𝐴)) “ {(0g‘𝐶)}) = {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (0g‘𝐶)} |
| 40 | 39 | eqcomi 2746 |
. . . . . . 7
⊢ {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (0g‘𝐶)} = (◡(𝑦 ∈ 𝐺 ↦ (𝑦 ↾ 𝐴)) “ {(0g‘𝐶)}) |
| 41 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐶) = (0g‘𝐶) |
| 42 | | eqid 2737 |
. . . . . . 7
⊢
(LSubSp‘𝐸) =
(LSubSp‘𝐸) |
| 43 | 40, 41, 42 | lmhmkerlss 21050 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐺 ↦ (𝑦 ↾ 𝐴)) ∈ (𝐸 LMHom 𝐶) → {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (0g‘𝐶)} ∈ (LSubSp‘𝐸)) |
| 44 | 36, 43 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (0g‘𝐶)} ∈ (LSubSp‘𝐸)) |
| 45 | 31, 44 | eqeltrd 2841 |
. . . 4
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐾 ∈ (LSubSp‘𝐸)) |
| 46 | | pwssplit4.l |
. . . . 5
⊢ 𝐿 = (𝐸 ↾s 𝐾) |
| 47 | 42, 46 | reslmhm 21051 |
. . . 4
⊢ (((𝑥 ∈ 𝐺 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐸 LMHom 𝐷) ∧ 𝐾 ∈ (LSubSp‘𝐸)) → ((𝑥 ∈ 𝐺 ↦ (𝑥 ↾ 𝐵)) ↾ 𝐾) ∈ (𝐿 LMHom 𝐷)) |
| 48 | 16, 45, 47 | syl2anc 584 |
. . 3
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑥 ∈ 𝐺 ↦ (𝑥 ↾ 𝐵)) ↾ 𝐾) ∈ (𝐿 LMHom 𝐷)) |
| 49 | 7, 48 | eqeltrid 2845 |
. 2
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐹 ∈ (𝐿 LMHom 𝐷)) |
| 50 | 1 | fvtresfn 7018 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐾 → (𝐹‘𝑎) = (𝑎 ↾ 𝐵)) |
| 51 | | ssexg 5323 |
. . . . . . . . . . 11
⊢ ((𝐵 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ∈ 𝑉) → 𝐵 ∈ V) |
| 52 | 8, 51 | mpan 690 |
. . . . . . . . . 10
⊢ ((𝐴 ∪ 𝐵) ∈ 𝑉 → 𝐵 ∈ V) |
| 53 | 52 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ∈ V) |
| 54 | 11, 26 | pws0g 18786 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ 𝐵 ∈ V) → (𝐵 × { 0 }) =
(0g‘𝐷)) |
| 55 | 20, 53, 54 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐵 × { 0 }) =
(0g‘𝐷)) |
| 56 | 55 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) →
(0g‘𝐷) =
(𝐵 × { 0
})) |
| 57 | 50, 56 | eqeqan12rd 2752 |
. . . . . 6
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ 𝐾) → ((𝐹‘𝑎) = (0g‘𝐷) ↔ (𝑎 ↾ 𝐵) = (𝐵 × { 0 }))) |
| 58 | | reseq1 5991 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑎 → (𝑦 ↾ 𝐴) = (𝑎 ↾ 𝐴)) |
| 59 | 58 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → ((𝑦 ↾ 𝐴) = (𝐴 × { 0 }) ↔ (𝑎 ↾ 𝐴) = (𝐴 × { 0 }))) |
| 60 | 59, 2 | elrab2 3695 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐾 ↔ (𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 }))) |
| 61 | | uneq12 4163 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ↾ 𝐴) = (𝐴 × { 0 }) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 })) → ((𝑎 ↾ 𝐴) ∪ (𝑎 ↾ 𝐵)) = ((𝐴 × { 0 }) ∪ (𝐵 × { 0 }))) |
| 62 | | resundi 6011 |
. . . . . . . . . . . . 13
⊢ (𝑎 ↾ (𝐴 ∪ 𝐵)) = ((𝑎 ↾ 𝐴) ∪ (𝑎 ↾ 𝐵)) |
| 63 | | xpundir 5755 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∪ 𝐵) × { 0 }) = ((𝐴 × { 0 }) ∪ (𝐵 × { 0 })) |
| 64 | 61, 62, 63 | 3eqtr4g 2802 |
. . . . . . . . . . . 12
⊢ (((𝑎 ↾ 𝐴) = (𝐴 × { 0 }) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 })) → (𝑎 ↾ (𝐴 ∪ 𝐵)) = ((𝐴 ∪ 𝐵) × { 0 })) |
| 65 | 64 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 })) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 })) → (𝑎 ↾ (𝐴 ∪ 𝐵)) = ((𝐴 ∪ 𝐵) × { 0 })) |
| 66 | 65 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 })) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 }))) → (𝑎 ↾ (𝐴 ∪ 𝐵)) = ((𝐴 ∪ 𝐵) × { 0 })) |
| 67 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 68 | | simpl1 1192 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 })) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 }))) → 𝑅 ∈ LMod) |
| 69 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ 𝑉) |
| 70 | 69 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 })) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 }))) → (𝐴 ∪ 𝐵) ∈ 𝑉) |
| 71 | | simprll 779 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 })) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 }))) → 𝑎 ∈ 𝐺) |
| 72 | 10, 67, 12, 68, 70, 71 | pwselbas 17534 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 })) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 }))) → 𝑎:(𝐴 ∪ 𝐵)⟶(Base‘𝑅)) |
| 73 | | ffn 6736 |
. . . . . . . . . . 11
⊢ (𝑎:(𝐴 ∪ 𝐵)⟶(Base‘𝑅) → 𝑎 Fn (𝐴 ∪ 𝐵)) |
| 74 | | fnresdm 6687 |
. . . . . . . . . . 11
⊢ (𝑎 Fn (𝐴 ∪ 𝐵) → (𝑎 ↾ (𝐴 ∪ 𝐵)) = 𝑎) |
| 75 | 72, 73, 74 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 })) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 }))) → (𝑎 ↾ (𝐴 ∪ 𝐵)) = 𝑎) |
| 76 | 10, 26 | pws0g 18786 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Mnd ∧ (𝐴 ∪ 𝐵) ∈ 𝑉) → ((𝐴 ∪ 𝐵) × { 0 }) =
(0g‘𝐸)) |
| 77 | 20, 69, 76 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) × { 0 }) =
(0g‘𝐸)) |
| 78 | 10 | pwslmod 20968 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉) → 𝐸 ∈ LMod) |
| 79 | 78 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐸 ∈ LMod) |
| 80 | 42 | lsssubg 20955 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 ∈ LMod ∧ 𝐾 ∈ (LSubSp‘𝐸)) → 𝐾 ∈ (SubGrp‘𝐸)) |
| 81 | 79, 45, 80 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐾 ∈ (SubGrp‘𝐸)) |
| 82 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐸) = (0g‘𝐸) |
| 83 | 46, 82 | subg0 19150 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ (SubGrp‘𝐸) →
(0g‘𝐸) =
(0g‘𝐿)) |
| 84 | 81, 83 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) →
(0g‘𝐸) =
(0g‘𝐿)) |
| 85 | 77, 84 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) × { 0 }) =
(0g‘𝐿)) |
| 86 | 85 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 })) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 }))) → ((𝐴 ∪ 𝐵) × { 0 }) =
(0g‘𝐿)) |
| 87 | 66, 75, 86 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 })) ∧ (𝑎 ↾ 𝐵) = (𝐵 × { 0 }))) → 𝑎 = (0g‘𝐿)) |
| 88 | 87 | exp32 420 |
. . . . . . . 8
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑎 ∈ 𝐺 ∧ (𝑎 ↾ 𝐴) = (𝐴 × { 0 })) → ((𝑎 ↾ 𝐵) = (𝐵 × { 0 }) → 𝑎 = (0g‘𝐿)))) |
| 89 | 60, 88 | biimtrid 242 |
. . . . . . 7
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑎 ∈ 𝐾 → ((𝑎 ↾ 𝐵) = (𝐵 × { 0 }) → 𝑎 = (0g‘𝐿)))) |
| 90 | 89 | imp 406 |
. . . . . 6
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ 𝐾) → ((𝑎 ↾ 𝐵) = (𝐵 × { 0 }) → 𝑎 = (0g‘𝐿))) |
| 91 | 57, 90 | sylbid 240 |
. . . . 5
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ 𝐾) → ((𝐹‘𝑎) = (0g‘𝐷) → 𝑎 = (0g‘𝐿))) |
| 92 | 91 | ralrimiva 3146 |
. . . 4
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → ∀𝑎 ∈ 𝐾 ((𝐹‘𝑎) = (0g‘𝐷) → 𝑎 = (0g‘𝐿))) |
| 93 | | lmghm 21030 |
. . . . 5
⊢ (𝐹 ∈ (𝐿 LMHom 𝐷) → 𝐹 ∈ (𝐿 GrpHom 𝐷)) |
| 94 | 46, 12 | ressbas2 17283 |
. . . . . . 7
⊢ (𝐾 ⊆ 𝐺 → 𝐾 = (Base‘𝐿)) |
| 95 | 4, 94 | ax-mp 5 |
. . . . . 6
⊢ 𝐾 = (Base‘𝐿) |
| 96 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝐿) = (0g‘𝐿) |
| 97 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝐷) = (0g‘𝐷) |
| 98 | 95, 13, 96, 97 | ghmf1 19264 |
. . . . 5
⊢ (𝐹 ∈ (𝐿 GrpHom 𝐷) → (𝐹:𝐾–1-1→(Base‘𝐷) ↔ ∀𝑎 ∈ 𝐾 ((𝐹‘𝑎) = (0g‘𝐷) → 𝑎 = (0g‘𝐿)))) |
| 99 | 49, 93, 98 | 3syl 18 |
. . . 4
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹:𝐾–1-1→(Base‘𝐷) ↔ ∀𝑎 ∈ 𝐾 ((𝐹‘𝑎) = (0g‘𝐷) → 𝑎 = (0g‘𝐿)))) |
| 100 | 92, 99 | mpbird 257 |
. . 3
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐹:𝐾–1-1→(Base‘𝐷)) |
| 101 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐿) =
(Base‘𝐿) |
| 102 | 101, 13 | lmhmf 21033 |
. . . . 5
⊢ (𝐹 ∈ (𝐿 LMHom 𝐷) → 𝐹:(Base‘𝐿)⟶(Base‘𝐷)) |
| 103 | | frn 6743 |
. . . . 5
⊢ (𝐹:(Base‘𝐿)⟶(Base‘𝐷) → ran 𝐹 ⊆ (Base‘𝐷)) |
| 104 | 49, 102, 103 | 3syl 18 |
. . . 4
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → ran 𝐹 ⊆ (Base‘𝐷)) |
| 105 | | reseq1 5991 |
. . . . . . 7
⊢ (𝑥 = (𝑎 ∪ (𝐴 × { 0 })) → (𝑥 ↾ 𝐵) = ((𝑎 ∪ (𝐴 × { 0 })) ↾ 𝐵)) |
| 106 | 11, 67, 13 | pwselbasb 17533 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ LMod ∧ 𝐵 ∈ V) → (𝑎 ∈ (Base‘𝐷) ↔ 𝑎:𝐵⟶(Base‘𝑅))) |
| 107 | 17, 53, 106 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑎 ∈ (Base‘𝐷) ↔ 𝑎:𝐵⟶(Base‘𝑅))) |
| 108 | 107 | biimpa 476 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → 𝑎:𝐵⟶(Base‘𝑅)) |
| 109 | 26 | fvexi 6920 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
| 110 | 109 | fconst 6794 |
. . . . . . . . . . . . 13
⊢ (𝐴 × { 0 }):𝐴⟶{ 0 } |
| 111 | 110 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝐴 × { 0 }):𝐴⟶{ 0 }) |
| 112 | 20 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → 𝑅 ∈ Mnd) |
| 113 | 67, 26 | mndidcl 18762 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Mnd → 0 ∈
(Base‘𝑅)) |
| 114 | 112, 113 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → 0 ∈ (Base‘𝑅)) |
| 115 | 114 | snssd 4809 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → { 0 } ⊆
(Base‘𝑅)) |
| 116 | 111, 115 | fssd 6753 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝐴 × { 0 }):𝐴⟶(Base‘𝑅)) |
| 117 | | incom 4209 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) |
| 118 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) = ∅) |
| 119 | 117, 118 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐵 ∩ 𝐴) = ∅) |
| 120 | 119 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝐵 ∩ 𝐴) = ∅) |
| 121 | | fun 6770 |
. . . . . . . . . . 11
⊢ (((𝑎:𝐵⟶(Base‘𝑅) ∧ (𝐴 × { 0 }):𝐴⟶(Base‘𝑅)) ∧ (𝐵 ∩ 𝐴) = ∅) → (𝑎 ∪ (𝐴 × { 0 })):(𝐵 ∪ 𝐴)⟶((Base‘𝑅) ∪ (Base‘𝑅))) |
| 122 | 108, 116,
120, 121 | syl21anc 838 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝑎 ∪ (𝐴 × { 0 })):(𝐵 ∪ 𝐴)⟶((Base‘𝑅) ∪ (Base‘𝑅))) |
| 123 | | uncom 4158 |
. . . . . . . . . . 11
⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) |
| 124 | | unidm 4157 |
. . . . . . . . . . 11
⊢
((Base‘𝑅)
∪ (Base‘𝑅)) =
(Base‘𝑅) |
| 125 | 123, 124 | feq23i 6730 |
. . . . . . . . . 10
⊢ ((𝑎 ∪ (𝐴 × { 0 })):(𝐵 ∪ 𝐴)⟶((Base‘𝑅) ∪ (Base‘𝑅)) ↔ (𝑎 ∪ (𝐴 × { 0 })):(𝐴 ∪ 𝐵)⟶(Base‘𝑅)) |
| 126 | 122, 125 | sylib 218 |
. . . . . . . . 9
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝑎 ∪ (𝐴 × { 0 })):(𝐴 ∪ 𝐵)⟶(Base‘𝑅)) |
| 127 | 10, 67, 12 | pwselbasb 17533 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉) → ((𝑎 ∪ (𝐴 × { 0 })) ∈ 𝐺 ↔ (𝑎 ∪ (𝐴 × { 0 })):(𝐴 ∪ 𝐵)⟶(Base‘𝑅))) |
| 128 | 127 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑎 ∪ (𝐴 × { 0 })) ∈ 𝐺 ↔ (𝑎 ∪ (𝐴 × { 0 })):(𝐴 ∪ 𝐵)⟶(Base‘𝑅))) |
| 129 | 128 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → ((𝑎 ∪ (𝐴 × { 0 })) ∈ 𝐺 ↔ (𝑎 ∪ (𝐴 × { 0 })):(𝐴 ∪ 𝐵)⟶(Base‘𝑅))) |
| 130 | 126, 129 | mpbird 257 |
. . . . . . . 8
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝑎 ∪ (𝐴 × { 0 })) ∈ 𝐺) |
| 131 | | simpl3 1194 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝐴 ∩ 𝐵) = ∅) |
| 132 | 117, 131 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝐵 ∩ 𝐴) = ∅) |
| 133 | | ffn 6736 |
. . . . . . . . . . . 12
⊢ (𝑎:𝐵⟶(Base‘𝑅) → 𝑎 Fn 𝐵) |
| 134 | | fnresdisj 6688 |
. . . . . . . . . . . 12
⊢ (𝑎 Fn 𝐵 → ((𝐵 ∩ 𝐴) = ∅ ↔ (𝑎 ↾ 𝐴) = ∅)) |
| 135 | 108, 133,
134 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → ((𝐵 ∩ 𝐴) = ∅ ↔ (𝑎 ↾ 𝐴) = ∅)) |
| 136 | 132, 135 | mpbid 232 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝑎 ↾ 𝐴) = ∅) |
| 137 | | fnconstg 6796 |
. . . . . . . . . . . 12
⊢ ( 0 ∈ V
→ (𝐴 × { 0 }) Fn 𝐴) |
| 138 | | fnresdm 6687 |
. . . . . . . . . . . 12
⊢ ((𝐴 × { 0 }) Fn 𝐴 → ((𝐴 × { 0 }) ↾ 𝐴) = (𝐴 × { 0 })) |
| 139 | 109, 137,
138 | mp2b 10 |
. . . . . . . . . . 11
⊢ ((𝐴 × { 0 }) ↾ 𝐴) = (𝐴 × { 0 }) |
| 140 | 139 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → ((𝐴 × { 0 }) ↾ 𝐴) = (𝐴 × { 0 })) |
| 141 | 136, 140 | uneq12d 4169 |
. . . . . . . . 9
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → ((𝑎 ↾ 𝐴) ∪ ((𝐴 × { 0 }) ↾ 𝐴)) = (∅ ∪ (𝐴 × { 0 }))) |
| 142 | | resundir 6012 |
. . . . . . . . 9
⊢ ((𝑎 ∪ (𝐴 × { 0 })) ↾ 𝐴) = ((𝑎 ↾ 𝐴) ∪ ((𝐴 × { 0 }) ↾ 𝐴)) |
| 143 | | uncom 4158 |
. . . . . . . . . 10
⊢ (∅
∪ (𝐴 × { 0 })) = ((𝐴 × { 0 }) ∪
∅) |
| 144 | | un0 4394 |
. . . . . . . . . 10
⊢ ((𝐴 × { 0 }) ∪ ∅) = (𝐴 × { 0 }) |
| 145 | 143, 144 | eqtr2i 2766 |
. . . . . . . . 9
⊢ (𝐴 × { 0 }) = (∅ ∪ (𝐴 × { 0 })) |
| 146 | 141, 142,
145 | 3eqtr4g 2802 |
. . . . . . . 8
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → ((𝑎 ∪ (𝐴 × { 0 })) ↾ 𝐴) = (𝐴 × { 0 })) |
| 147 | | reseq1 5991 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑎 ∪ (𝐴 × { 0 })) → (𝑦 ↾ 𝐴) = ((𝑎 ∪ (𝐴 × { 0 })) ↾ 𝐴)) |
| 148 | 147 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑦 = (𝑎 ∪ (𝐴 × { 0 })) → ((𝑦 ↾ 𝐴) = (𝐴 × { 0 }) ↔ ((𝑎 ∪ (𝐴 × { 0 })) ↾ 𝐴) = (𝐴 × { 0 }))) |
| 149 | 148, 2 | elrab2 3695 |
. . . . . . . 8
⊢ ((𝑎 ∪ (𝐴 × { 0 })) ∈ 𝐾 ↔ ((𝑎 ∪ (𝐴 × { 0 })) ∈ 𝐺 ∧ ((𝑎 ∪ (𝐴 × { 0 })) ↾ 𝐴) = (𝐴 × { 0 }))) |
| 150 | 130, 146,
149 | sylanbrc 583 |
. . . . . . 7
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝑎 ∪ (𝐴 × { 0 })) ∈ 𝐾) |
| 151 | 130 | resexd 6046 |
. . . . . . 7
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → ((𝑎 ∪ (𝐴 × { 0 })) ↾ 𝐵) ∈ V) |
| 152 | 1, 105, 150, 151 | fvmptd3 7039 |
. . . . . 6
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝐹‘(𝑎 ∪ (𝐴 × { 0 }))) = ((𝑎 ∪ (𝐴 × { 0 })) ↾ 𝐵)) |
| 153 | | resundir 6012 |
. . . . . . 7
⊢ ((𝑎 ∪ (𝐴 × { 0 })) ↾ 𝐵) = ((𝑎 ↾ 𝐵) ∪ ((𝐴 × { 0 }) ↾ 𝐵)) |
| 154 | | fnresdm 6687 |
. . . . . . . . . 10
⊢ (𝑎 Fn 𝐵 → (𝑎 ↾ 𝐵) = 𝑎) |
| 155 | 108, 133,
154 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝑎 ↾ 𝐵) = 𝑎) |
| 156 | | ffn 6736 |
. . . . . . . . . . . . 13
⊢ ((𝐴 × { 0 }):𝐴⟶{ 0 } → (𝐴 × { 0 }) Fn 𝐴) |
| 157 | | fnresdisj 6688 |
. . . . . . . . . . . . 13
⊢ ((𝐴 × { 0 }) Fn 𝐴 → ((𝐴 ∩ 𝐵) = ∅ ↔ ((𝐴 × { 0 }) ↾ 𝐵) = ∅)) |
| 158 | 110, 156,
157 | mp2b 10 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ((𝐴 × { 0 }) ↾ 𝐵) = ∅) |
| 159 | 158 | biimpi 216 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × { 0 }) ↾ 𝐵) = ∅) |
| 160 | 159 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 × { 0 }) ↾ 𝐵) = ∅) |
| 161 | 160 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → ((𝐴 × { 0 }) ↾ 𝐵) = ∅) |
| 162 | 155, 161 | uneq12d 4169 |
. . . . . . . 8
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → ((𝑎 ↾ 𝐵) ∪ ((𝐴 × { 0 }) ↾ 𝐵)) = (𝑎 ∪ ∅)) |
| 163 | | un0 4394 |
. . . . . . . 8
⊢ (𝑎 ∪ ∅) = 𝑎 |
| 164 | 162, 163 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → ((𝑎 ↾ 𝐵) ∪ ((𝐴 × { 0 }) ↾ 𝐵)) = 𝑎) |
| 165 | 153, 164 | eqtrid 2789 |
. . . . . 6
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → ((𝑎 ∪ (𝐴 × { 0 })) ↾ 𝐵) = 𝑎) |
| 166 | 152, 165 | eqtrd 2777 |
. . . . 5
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝐹‘(𝑎 ∪ (𝐴 × { 0 }))) = 𝑎) |
| 167 | 95, 13 | lmhmf 21033 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐿 LMHom 𝐷) → 𝐹:𝐾⟶(Base‘𝐷)) |
| 168 | | ffn 6736 |
. . . . . . . 8
⊢ (𝐹:𝐾⟶(Base‘𝐷) → 𝐹 Fn 𝐾) |
| 169 | 49, 167, 168 | 3syl 18 |
. . . . . . 7
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐹 Fn 𝐾) |
| 170 | 169 | adantr 480 |
. . . . . 6
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → 𝐹 Fn 𝐾) |
| 171 | | fnfvelrn 7100 |
. . . . . 6
⊢ ((𝐹 Fn 𝐾 ∧ (𝑎 ∪ (𝐴 × { 0 })) ∈ 𝐾) → (𝐹‘(𝑎 ∪ (𝐴 × { 0 }))) ∈ ran 𝐹) |
| 172 | 170, 150,
171 | syl2anc 584 |
. . . . 5
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → (𝐹‘(𝑎 ∪ (𝐴 × { 0 }))) ∈ ran 𝐹) |
| 173 | 166, 172 | eqeltrrd 2842 |
. . . 4
⊢ (((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑎 ∈ (Base‘𝐷)) → 𝑎 ∈ ran 𝐹) |
| 174 | 104, 173 | eqelssd 4005 |
. . 3
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → ran 𝐹 = (Base‘𝐷)) |
| 175 | | dff1o5 6857 |
. . 3
⊢ (𝐹:𝐾–1-1-onto→(Base‘𝐷) ↔ (𝐹:𝐾–1-1→(Base‘𝐷) ∧ ran 𝐹 = (Base‘𝐷))) |
| 176 | 100, 174,
175 | sylanbrc 583 |
. 2
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐹:𝐾–1-1-onto→(Base‘𝐷)) |
| 177 | 95, 13 | islmim 21061 |
. 2
⊢ (𝐹 ∈ (𝐿 LMIso 𝐷) ↔ (𝐹 ∈ (𝐿 LMHom 𝐷) ∧ 𝐹:𝐾–1-1-onto→(Base‘𝐷))) |
| 178 | 49, 176, 177 | sylanbrc 583 |
1
⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐹 ∈ (𝐿 LMIso 𝐷)) |