Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑀 ∈ LMod) |
2 | 1 | 3ad2ant1 1134 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ LMod) |
3 | | lincvalsn.r |
. . . . . . . . 9
⊢ 𝑅 = (Base‘𝑆) |
4 | | lincvalsn.s |
. . . . . . . . . 10
⊢ 𝑆 = (Scalar‘𝑀) |
5 | 4 | fveq2i 6677 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘(Scalar‘𝑀)) |
6 | 3, 5 | eqtri 2761 |
. . . . . . . 8
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
7 | 6 | eleq2i 2824 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ (Base‘(Scalar‘𝑀))) |
8 | 7 | biimpi 219 |
. . . . . 6
⊢ (𝑋 ∈ 𝑅 → 𝑋 ∈ (Base‘(Scalar‘𝑀))) |
9 | 8 | anim2i 620 |
. . . . 5
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀)))) |
10 | 9 | 3ad2ant2 1135 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀)))) |
11 | 6 | eleq2i 2824 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑅 ↔ 𝑌 ∈ (Base‘(Scalar‘𝑀))) |
12 | 11 | biimpi 219 |
. . . . . 6
⊢ (𝑌 ∈ 𝑅 → 𝑌 ∈ (Base‘(Scalar‘𝑀))) |
13 | 12 | anim2i 620 |
. . . . 5
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀)))) |
14 | 13 | 3ad2ant3 1136 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀)))) |
15 | | fvexd 6689 |
. . . . . . 7
⊢ (𝑀 ∈ LMod →
(Base‘(Scalar‘𝑀)) ∈ V) |
16 | 15 | anim2i 620 |
. . . . . 6
⊢ ((𝑉 ≠ 𝑊 ∧ 𝑀 ∈ LMod) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) |
17 | 16 | ancoms 462 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) |
18 | 17 | 3ad2ant1 1134 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) |
19 | | lincvalpr.f |
. . . . 5
⊢ 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉} |
20 | 19 | mapprop 45216 |
. . . 4
⊢ (((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀))) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀))) ∧ (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) → 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m {𝑉, 𝑊})) |
21 | 10, 14, 18, 20 | syl3anc 1372 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑉, 𝑊})) |
22 | | lincvalsn.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑀) |
23 | 22 | eleq2i 2824 |
. . . . . . 7
⊢ (𝑉 ∈ 𝐵 ↔ 𝑉 ∈ (Base‘𝑀)) |
24 | 23 | biimpi 219 |
. . . . . 6
⊢ (𝑉 ∈ 𝐵 → 𝑉 ∈ (Base‘𝑀)) |
25 | 24 | adantr 484 |
. . . . 5
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑉 ∈ (Base‘𝑀)) |
26 | 22 | eleq2i 2824 |
. . . . . . 7
⊢ (𝑊 ∈ 𝐵 ↔ 𝑊 ∈ (Base‘𝑀)) |
27 | 26 | biimpi 219 |
. . . . . 6
⊢ (𝑊 ∈ 𝐵 → 𝑊 ∈ (Base‘𝑀)) |
28 | 27 | adantr 484 |
. . . . 5
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑊 ∈ (Base‘𝑀)) |
29 | | prelpwi 5306 |
. . . . 5
⊢ ((𝑉 ∈ (Base‘𝑀) ∧ 𝑊 ∈ (Base‘𝑀)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) |
30 | 25, 28, 29 | syl2an 599 |
. . . 4
⊢ (((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) |
31 | 30 | 3adant1 1131 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) |
32 | | lincval 45284 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m {𝑉, 𝑊}) ∧ {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
33 | 2, 21, 31, 32 | syl3anc 1372 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
34 | | lmodcmn 19801 |
. . . . 5
⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd) |
35 | 34 | adantr 484 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑀 ∈ CMnd) |
36 | 35 | 3ad2ant1 1134 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ CMnd) |
37 | | simpr 488 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑉 ≠ 𝑊) |
38 | | simpl 486 |
. . . . 5
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑉 ∈ 𝐵) |
39 | | simpl 486 |
. . . . 5
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑊 ∈ 𝐵) |
40 | 37, 38, 39 | 3anim123i 1152 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) |
41 | | 3anrot 1101 |
. . . 4
⊢ ((𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ↔ (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊)) |
42 | 40, 41 | sylib 221 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊)) |
43 | 19 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}) |
44 | 43 | fveq1d 6676 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝐹‘𝑉) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉)) |
45 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑉 ∈ 𝐵) |
46 | | simprr 773 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑋 ∈ 𝑅) |
47 | 37 | adantr 484 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑉 ≠ 𝑊) |
48 | | fvpr1g 6964 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) = 𝑋) |
49 | 45, 46, 47, 48 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) = 𝑋) |
50 | 44, 49 | eqtrd 2773 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝐹‘𝑉) = 𝑋) |
51 | 50 | oveq1d 7185 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) = (𝑋( ·𝑠
‘𝑀)𝑉)) |
52 | 1 | adantr 484 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑀 ∈ LMod) |
53 | | eqid 2738 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
54 | 22, 4, 53, 3 | lmodvscl 19770 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ∈ 𝐵) → (𝑋( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
55 | 52, 46, 45, 54 | syl3anc 1372 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝑋( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
56 | 51, 55 | eqeltrd 2833 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
57 | 56 | 3adant3 1133 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
58 | 19 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}) |
59 | 58 | fveq1d 6676 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊)) |
60 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 ∈ 𝐵) |
61 | | simprr 773 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅) |
62 | 37 | adantr 484 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ≠ 𝑊) |
63 | | fvpr2g 6965 |
. . . . . . . 8
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) = 𝑌) |
64 | 60, 61, 62, 63 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) = 𝑌) |
65 | 59, 64 | eqtrd 2773 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = 𝑌) |
66 | 65 | oveq1d 7185 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) = (𝑌( ·𝑠
‘𝑀)𝑊)) |
67 | 1 | adantr 484 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ LMod) |
68 | 22, 4, 53, 3 | lmodvscl 19770 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑌 ∈ 𝑅 ∧ 𝑊 ∈ 𝐵) → (𝑌( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
69 | 67, 61, 60, 68 | syl3anc 1372 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑌( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
70 | 66, 69 | eqeltrd 2833 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
71 | 70 | 3adant2 1132 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
72 | | lincvalpr.p |
. . . 4
⊢ + =
(+g‘𝑀) |
73 | | fveq2 6674 |
. . . . 5
⊢ (𝑣 = 𝑉 → (𝐹‘𝑣) = (𝐹‘𝑉)) |
74 | | id 22 |
. . . . 5
⊢ (𝑣 = 𝑉 → 𝑣 = 𝑉) |
75 | 73, 74 | oveq12d 7188 |
. . . 4
⊢ (𝑣 = 𝑉 → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉)) |
76 | | fveq2 6674 |
. . . . 5
⊢ (𝑣 = 𝑊 → (𝐹‘𝑣) = (𝐹‘𝑊)) |
77 | | id 22 |
. . . . 5
⊢ (𝑣 = 𝑊 → 𝑣 = 𝑊) |
78 | 76, 77 | oveq12d 7188 |
. . . 4
⊢ (𝑣 = 𝑊 → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊)) |
79 | 22, 72, 75, 78 | gsumpr 19194 |
. . 3
⊢ ((𝑀 ∈ CMnd ∧ (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊) ∧ (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) ∈ 𝐵 ∧ ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) ∈ 𝐵)) → (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) = (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊))) |
80 | 36, 42, 57, 71, 79 | syl112anc 1375 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) = (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊))) |
81 | | lincvalsn.t |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑀) |
82 | 81 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → · = (
·𝑠 ‘𝑀)) |
83 | 82 | eqcomd 2744 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (
·𝑠 ‘𝑀) = · ) |
84 | 19 | fveq1i 6675 |
. . . . 5
⊢ (𝐹‘𝑉) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) |
85 | 38 | 3ad2ant2 1135 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ∈ 𝐵) |
86 | | simpr 488 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑋 ∈ 𝑅) |
87 | 86 | 3ad2ant2 1135 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑋 ∈ 𝑅) |
88 | 37 | 3ad2ant1 1134 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ≠ 𝑊) |
89 | 85, 87, 88, 48 | syl3anc 1372 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) = 𝑋) |
90 | 84, 89 | syl5eq 2785 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑉) = 𝑋) |
91 | | eqidd 2739 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 = 𝑉) |
92 | 83, 90, 91 | oveq123d 7191 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) = (𝑋 · 𝑉)) |
93 | 19 | fveq1i 6675 |
. . . . 5
⊢ (𝐹‘𝑊) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) |
94 | 39 | 3ad2ant3 1136 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 ∈ 𝐵) |
95 | | simpr 488 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑌 ∈ 𝑅) |
96 | 95 | 3ad2ant3 1136 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅) |
97 | 94, 96, 88, 63 | syl3anc 1372 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) = 𝑌) |
98 | 93, 97 | syl5eq 2785 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = 𝑌) |
99 | | eqidd 2739 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 = 𝑊) |
100 | 83, 98, 99 | oveq123d 7191 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) = (𝑌 · 𝑊)) |
101 | 92, 100 | oveq12d 7188 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊)) = ((𝑋 · 𝑉) + (𝑌 · 𝑊))) |
102 | 33, 80, 101 | 3eqtrd 2777 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = ((𝑋 · 𝑉) + (𝑌 · 𝑊))) |