Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑀 ∈ LMod) |
2 | 1 | 3ad2ant1 1075 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ LMod) |
3 | | lincvalsn.r |
. . . . . . . . 9
⊢ 𝑅 = (Base‘𝑆) |
4 | | lincvalsn.s |
. . . . . . . . . 10
⊢ 𝑆 = (Scalar‘𝑀) |
5 | 4 | fveq2i 6106 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘(Scalar‘𝑀)) |
6 | 3, 5 | eqtri 2632 |
. . . . . . . 8
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
7 | 6 | eleq2i 2680 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ (Base‘(Scalar‘𝑀))) |
8 | 7 | biimpi 205 |
. . . . . 6
⊢ (𝑋 ∈ 𝑅 → 𝑋 ∈ (Base‘(Scalar‘𝑀))) |
9 | 8 | anim2i 591 |
. . . . 5
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀)))) |
10 | 9 | 3ad2ant2 1076 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀)))) |
11 | 6 | eleq2i 2680 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑅 ↔ 𝑌 ∈ (Base‘(Scalar‘𝑀))) |
12 | 11 | biimpi 205 |
. . . . . 6
⊢ (𝑌 ∈ 𝑅 → 𝑌 ∈ (Base‘(Scalar‘𝑀))) |
13 | 12 | anim2i 591 |
. . . . 5
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀)))) |
14 | 13 | 3ad2ant3 1077 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀)))) |
15 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
16 | 15 | a1i 11 |
. . . . . . 7
⊢ (𝑀 ∈ LMod →
(Base‘(Scalar‘𝑀)) ∈ V) |
17 | 16 | anim2i 591 |
. . . . . 6
⊢ ((𝑉 ≠ 𝑊 ∧ 𝑀 ∈ LMod) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) |
18 | 17 | ancoms 468 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) |
19 | 18 | 3ad2ant1 1075 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) |
20 | | lincvalpr.f |
. . . . 5
⊢ 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉} |
21 | 20 | mapprop 41917 |
. . . 4
⊢ (((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀))) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀))) ∧ (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) → 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 {𝑉, 𝑊})) |
22 | 10, 14, 19, 21 | syl3anc 1318 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
{𝑉, 𝑊})) |
23 | | lincvalsn.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑀) |
24 | 23 | eleq2i 2680 |
. . . . . . 7
⊢ (𝑉 ∈ 𝐵 ↔ 𝑉 ∈ (Base‘𝑀)) |
25 | 24 | biimpi 205 |
. . . . . 6
⊢ (𝑉 ∈ 𝐵 → 𝑉 ∈ (Base‘𝑀)) |
26 | 25 | adantr 480 |
. . . . 5
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑉 ∈ (Base‘𝑀)) |
27 | 23 | eleq2i 2680 |
. . . . . . 7
⊢ (𝑊 ∈ 𝐵 ↔ 𝑊 ∈ (Base‘𝑀)) |
28 | 27 | biimpi 205 |
. . . . . 6
⊢ (𝑊 ∈ 𝐵 → 𝑊 ∈ (Base‘𝑀)) |
29 | 28 | adantr 480 |
. . . . 5
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑊 ∈ (Base‘𝑀)) |
30 | | prelpwi 4842 |
. . . . 5
⊢ ((𝑉 ∈ (Base‘𝑀) ∧ 𝑊 ∈ (Base‘𝑀)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) |
31 | 26, 29, 30 | syl2an 493 |
. . . 4
⊢ (((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) |
32 | 31 | 3adant1 1072 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) |
33 | | lincval 41992 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 {𝑉, 𝑊}) ∧ {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
34 | 2, 22, 32, 33 | syl3anc 1318 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
35 | | lmodcmn 18734 |
. . . . 5
⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd) |
36 | 35 | adantr 480 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑀 ∈ CMnd) |
37 | 36 | 3ad2ant1 1075 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ CMnd) |
38 | | simpr 476 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑉 ≠ 𝑊) |
39 | | simpl 472 |
. . . . 5
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑉 ∈ 𝐵) |
40 | | simpl 472 |
. . . . 5
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑊 ∈ 𝐵) |
41 | 38, 39, 40 | 3anim123i 1240 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) |
42 | | 3anrot 1036 |
. . . 4
⊢ ((𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ↔ (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊)) |
43 | 41, 42 | sylib 207 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊)) |
44 | 20 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}) |
45 | 44 | fveq1d 6105 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝐹‘𝑉) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉)) |
46 | | simprl 790 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑉 ∈ 𝐵) |
47 | | simprr 792 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑋 ∈ 𝑅) |
48 | 38 | adantr 480 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑉 ≠ 𝑊) |
49 | | fvpr1g 6363 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) = 𝑋) |
50 | 46, 47, 48, 49 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) = 𝑋) |
51 | 45, 50 | eqtrd 2644 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝐹‘𝑉) = 𝑋) |
52 | 51 | oveq1d 6564 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) = (𝑋( ·𝑠
‘𝑀)𝑉)) |
53 | 1 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑀 ∈ LMod) |
54 | | eqid 2610 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
55 | 23, 4, 54, 3 | lmodvscl 18703 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ∈ 𝐵) → (𝑋( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
56 | 53, 47, 46, 55 | syl3anc 1318 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝑋( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
57 | 52, 56 | eqeltrd 2688 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
58 | 57 | 3adant3 1074 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) ∈ 𝐵) |
59 | 20 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}) |
60 | 59 | fveq1d 6105 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊)) |
61 | | simprl 790 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 ∈ 𝐵) |
62 | | simprr 792 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅) |
63 | 38 | adantr 480 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ≠ 𝑊) |
64 | | fvpr2g 6364 |
. . . . . . . 8
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) = 𝑌) |
65 | 61, 62, 63, 64 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) = 𝑌) |
66 | 60, 65 | eqtrd 2644 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = 𝑌) |
67 | 66 | oveq1d 6564 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) = (𝑌( ·𝑠
‘𝑀)𝑊)) |
68 | 1 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ LMod) |
69 | 23, 4, 54, 3 | lmodvscl 18703 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑌 ∈ 𝑅 ∧ 𝑊 ∈ 𝐵) → (𝑌( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
70 | 68, 62, 61, 69 | syl3anc 1318 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑌( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
71 | 67, 70 | eqeltrd 2688 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
72 | 71 | 3adant2 1073 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) ∈ 𝐵) |
73 | | lincvalpr.p |
. . . 4
⊢ + =
(+g‘𝑀) |
74 | | fveq2 6103 |
. . . . 5
⊢ (𝑣 = 𝑉 → (𝐹‘𝑣) = (𝐹‘𝑉)) |
75 | | id 22 |
. . . . 5
⊢ (𝑣 = 𝑉 → 𝑣 = 𝑉) |
76 | 74, 75 | oveq12d 6567 |
. . . 4
⊢ (𝑣 = 𝑉 → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉)) |
77 | | fveq2 6103 |
. . . . 5
⊢ (𝑣 = 𝑊 → (𝐹‘𝑣) = (𝐹‘𝑊)) |
78 | | id 22 |
. . . . 5
⊢ (𝑣 = 𝑊 → 𝑣 = 𝑊) |
79 | 77, 78 | oveq12d 6567 |
. . . 4
⊢ (𝑣 = 𝑊 → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊)) |
80 | 23, 73, 76, 79 | gsumpr 41932 |
. . 3
⊢ ((𝑀 ∈ CMnd ∧ (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊) ∧ (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) ∈ 𝐵 ∧ ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) ∈ 𝐵)) → (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) = (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊))) |
81 | 37, 43, 58, 72, 80 | syl112anc 1322 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) = (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊))) |
82 | | lincvalsn.t |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑀) |
83 | 82 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → · = (
·𝑠 ‘𝑀)) |
84 | 83 | eqcomd 2616 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (
·𝑠 ‘𝑀) = · ) |
85 | 20 | fveq1i 6104 |
. . . . 5
⊢ (𝐹‘𝑉) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) |
86 | 39 | 3ad2ant2 1076 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ∈ 𝐵) |
87 | | simpr 476 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑋 ∈ 𝑅) |
88 | 87 | 3ad2ant2 1076 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑋 ∈ 𝑅) |
89 | 38 | 3ad2ant1 1075 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ≠ 𝑊) |
90 | 86, 88, 89, 49 | syl3anc 1318 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑉) = 𝑋) |
91 | 85, 90 | syl5eq 2656 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑉) = 𝑋) |
92 | | eqidd 2611 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 = 𝑉) |
93 | 84, 91, 92 | oveq123d 6570 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) = (𝑋 · 𝑉)) |
94 | 20 | fveq1i 6104 |
. . . . 5
⊢ (𝐹‘𝑊) = ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) |
95 | 40 | 3ad2ant3 1077 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 ∈ 𝐵) |
96 | | simpr 476 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑌 ∈ 𝑅) |
97 | 96 | 3ad2ant3 1077 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅) |
98 | 95, 97, 89, 64 | syl3anc 1318 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉}‘𝑊) = 𝑌) |
99 | 94, 98 | syl5eq 2656 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = 𝑌) |
100 | | eqidd 2611 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 = 𝑊) |
101 | 84, 99, 100 | oveq123d 6570 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊) = (𝑌 · 𝑊)) |
102 | 93, 101 | oveq12d 6567 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (((𝐹‘𝑉)( ·𝑠
‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠
‘𝑀)𝑊)) = ((𝑋 · 𝑉) + (𝑌 · 𝑊))) |
103 | 34, 81, 102 | 3eqtrd 2648 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = ((𝑋 · 𝑉) + (𝑌 · 𝑊))) |