| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑀 ∈ LMod) |
| 2 | 1 | 3ad2ant1 1134 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ LMod) |
| 3 | | lincvalsn.r |
. . . . . . . . 9
⊢ 𝑅 = (Base‘𝑆) |
| 4 | | lincvalsn.s |
. . . . . . . . . 10
⊢ 𝑆 = (Scalar‘𝑀) |
| 5 | 4 | fveq2i 6909 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘(Scalar‘𝑀)) |
| 6 | 3, 5 | eqtri 2765 |
. . . . . . . 8
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
| 7 | 6 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ (Base‘(Scalar‘𝑀))) |
| 8 | 7 | biimpi 216 |
. . . . . 6
⊢ (𝑋 ∈ 𝑅 → 𝑋 ∈ (Base‘(Scalar‘𝑀))) |
| 9 | 8 | anim2i 617 |
. . . . 5
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀)))) |
| 10 | 9 | 3ad2ant2 1135 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀)))) |
| 11 | 6 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑅 ↔ 𝑌 ∈ (Base‘(Scalar‘𝑀))) |
| 12 | 11 | biimpi 216 |
. . . . . 6
⊢ (𝑌 ∈ 𝑅 → 𝑌 ∈ (Base‘(Scalar‘𝑀))) |
| 13 | 12 | anim2i 617 |
. . . . 5
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀)))) |
| 14 | 13 | 3ad2ant3 1136 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀)))) |
| 15 | | fvexd 6921 |
. . . . . . 7
⊢ (𝑀 ∈ LMod →
(Base‘(Scalar‘𝑀)) ∈ V) |
| 16 | 15 | anim2i 617 |
. . . . . 6
⊢ ((𝑉 ≠ 𝑊 ∧ 𝑀 ∈ LMod) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) |
| 17 | 16 | ancoms 458 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) |
| 18 | 17 | 3ad2ant1 1134 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) |
| 19 | | lincvalpr.f |
. . . . 5
⊢ 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉} |
| 20 | 19 | mapprop 48262 |
. . . 4
⊢ (((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀))) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀))) ∧ (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) → 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m {𝑉, 𝑊})) |
| 21 | 10, 14, 18, 20 | syl3anc 1373 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑉, 𝑊})) |
| 22 | | lincvalsn.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑀) |
| 23 | 22 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑉 ∈ 𝐵 ↔ 𝑉 ∈ (Base‘𝑀)) |
| 24 | 23 | biimpi 216 |
. . . . . 6
⊢ (𝑉 ∈ 𝐵 → 𝑉 ∈ (Base‘𝑀)) |
| 25 | 24 | adantr 480 |
. . . . 5
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑉 ∈ (Base‘𝑀)) |
| 26 | 22 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑊 ∈ 𝐵 ↔ 𝑊 ∈ (Base‘𝑀)) |
| 27 | 26 | biimpi 216 |
. . . . . 6
⊢ (𝑊 ∈ 𝐵 → 𝑊 ∈ (Base‘𝑀)) |
| 28 | 27 | adantr 480 |
. . . . 5
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑊 ∈ (Base‘𝑀)) |
| 29 | | prelpwi 5452 |
. . . . 5
⊢ ((𝑉 ∈ (Base‘𝑀) ∧ 𝑊 ∈ (Base‘𝑀)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) |
| 30 | 25, 28, 29 | syl2an 596 |
. . . 4
⊢ (((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) |
| 31 | 30 | 3adant1 1131 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) |
| 32 | | lincval 48326 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m {𝑉, 𝑊}) ∧ {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
| 33 | 2, 21, 31, 32 | syl3anc 1373 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
| 34 | | lmodcmn 20908 |
. . . . 5
⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd) |
| 35 | 34 | adantr 480 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑀 ∈ CMnd) |
| 36 | 35 | 3ad2ant1 1134 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ CMnd) |
| 37 | | simpr 484 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑉 ≠ 𝑊) |
| 38 | | simpl 482 |
. . . . 5
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑉 ∈ 𝐵) |
| 39 | | simpl 482 |
. . . . 5
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑊 ∈ 𝐵) |
| 40 | 37, 38, 39 | 3anim123i 1152 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) |
| 41 | | 3anrot 1100 |
. . . 4
⊢ ((𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ↔ (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊)) |
| 42 | 40, 41 | sylib 218 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊)) |
| 43 | 19 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}) |
| 44 | 43 | fveq1d 6908 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝐹‘𝑉) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉)) |
| 45 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑉 ∈ 𝐵) |
| 46 | | simprr 773 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑋 ∈ 𝑅) |
| 47 | 37 | adantr 480 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑉 ≠ 𝑊) |
| 48 | | fvpr1g 7210 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) = 𝑋) |
| 49 | 45, 46, 47, 48 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) = 𝑋) |
| 50 | 44, 49 | eqtrd 2777 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝐹‘𝑉) = 𝑋) |
| 51 | 50 | oveq1d 7446 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) = (𝑋( ·𝑠
‘𝑀)𝑉)) |
| 52 | 1 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑀 ∈ LMod) |
| 53 | | eqid 2737 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
| 54 | 22, 4, 53, 3 | lmodvscl 20876 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ∈ 𝐵) → (𝑋( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
| 55 | 52, 46, 45, 54 | syl3anc 1373 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝑋( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
| 56 | 51, 55 | eqeltrd 2841 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
| 57 | 56 | 3adant3 1133 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
| 58 | 19 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}) |
| 59 | 58 | fveq1d 6908 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊)) |
| 60 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 ∈ 𝐵) |
| 61 | | simprr 773 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅) |
| 62 | 37 | adantr 480 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ≠ 𝑊) |
| 63 | | fvpr2g 7211 |
. . . . . . . 8
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) = 𝑌) |
| 64 | 60, 61, 62, 63 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) = 𝑌) |
| 65 | 59, 64 | eqtrd 2777 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = 𝑌) |
| 66 | 65 | oveq1d 7446 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) = (𝑌( ·𝑠
‘𝑀)𝑊)) |
| 67 | 1 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ LMod) |
| 68 | 22, 4, 53, 3 | lmodvscl 20876 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑌 ∈ 𝑅 ∧ 𝑊 ∈ 𝐵) → (𝑌( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
| 69 | 67, 61, 60, 68 | syl3anc 1373 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑌( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
| 70 | 66, 69 | eqeltrd 2841 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
| 71 | 70 | 3adant2 1132 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
| 72 | | lincvalpr.p |
. . . 4
⊢ + =
(+g‘𝑀) |
| 73 | | fveq2 6906 |
. . . . 5
⊢ (𝑣 = 𝑉 → (𝐹‘𝑣) = (𝐹‘𝑉)) |
| 74 | | id 22 |
. . . . 5
⊢ (𝑣 = 𝑉 → 𝑣 = 𝑉) |
| 75 | 73, 74 | oveq12d 7449 |
. . . 4
⊢ (𝑣 = 𝑉 → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉)) |
| 76 | | fveq2 6906 |
. . . . 5
⊢ (𝑣 = 𝑊 → (𝐹‘𝑣) = (𝐹‘𝑊)) |
| 77 | | id 22 |
. . . . 5
⊢ (𝑣 = 𝑊 → 𝑣 = 𝑊) |
| 78 | 76, 77 | oveq12d 7449 |
. . . 4
⊢ (𝑣 = 𝑊 → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊)) |
| 79 | 22, 72, 75, 78 | gsumpr 19973 |
. . 3
⊢ ((𝑀 ∈ CMnd ∧ (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊) ∧ (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) ∈ 𝐵 ∧ ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) ∈ 𝐵)) → (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) = (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊))) |
| 80 | 36, 42, 57, 71, 79 | syl112anc 1376 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) = (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊))) |
| 81 | | lincvalsn.t |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑀) |
| 82 | 81 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → · = (
·𝑠 ‘𝑀)) |
| 83 | 82 | eqcomd 2743 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (
·𝑠 ‘𝑀) = · ) |
| 84 | 19 | fveq1i 6907 |
. . . . 5
⊢ (𝐹‘𝑉) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) |
| 85 | 38 | 3ad2ant2 1135 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ∈ 𝐵) |
| 86 | | simpr 484 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑋 ∈ 𝑅) |
| 87 | 86 | 3ad2ant2 1135 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑋 ∈ 𝑅) |
| 88 | 37 | 3ad2ant1 1134 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ≠ 𝑊) |
| 89 | 85, 87, 88, 48 | syl3anc 1373 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) = 𝑋) |
| 90 | 84, 89 | eqtrid 2789 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑉) = 𝑋) |
| 91 | | eqidd 2738 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 = 𝑉) |
| 92 | 83, 90, 91 | oveq123d 7452 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) = (𝑋 · 𝑉)) |
| 93 | 19 | fveq1i 6907 |
. . . . 5
⊢ (𝐹‘𝑊) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) |
| 94 | 39 | 3ad2ant3 1136 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 ∈ 𝐵) |
| 95 | | simpr 484 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑌 ∈ 𝑅) |
| 96 | 95 | 3ad2ant3 1136 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅) |
| 97 | 94, 96, 88, 63 | syl3anc 1373 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) = 𝑌) |
| 98 | 93, 97 | eqtrid 2789 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = 𝑌) |
| 99 | | eqidd 2738 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 = 𝑊) |
| 100 | 83, 98, 99 | oveq123d 7452 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) = (𝑌 · 𝑊)) |
| 101 | 92, 100 | oveq12d 7449 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊)) = ((𝑋 · 𝑉) + (𝑌 · 𝑊))) |
| 102 | 33, 80, 101 | 3eqtrd 2781 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = ((𝑋 · 𝑉) + (𝑌 · 𝑊))) |