Metamath Proof Explorer

Theorem isslmd

Description: The predicate "is a semimodule". (Contributed by NM, 4-Nov-2013) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses isslmd.v ⊢V=BaseW
isslmd.a ⊢+˙=+W
isslmd.s ⊢·˙=⋅W
isslmd.0 ⊢0˙=0W
isslmd.f ⊢F=Scalar⁡W
isslmd.k ⊢K=BaseF
isslmd.p ⊢⨣˙=+F
isslmd.t ⊢×˙=⋅F
isslmd.u ⊢1˙=1F
isslmd.o ⊢O=0F
Assertion isslmd ⊢W∈SLMod↔W∈CMnd∧F∈SRing∧∀q∈K∀r∈K∀x∈V∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙

Proof

Step Hyp Ref Expression
1 isslmd.v ⊢V=BaseW
2 isslmd.a ⊢+˙=+W
3 isslmd.s ⊢·˙=⋅W
4 isslmd.0 ⊢0˙=0W
5 isslmd.f ⊢F=Scalar⁡W
6 isslmd.k ⊢K=BaseF
7 isslmd.p ⊢⨣˙=+F
8 isslmd.t ⊢×˙=⋅F
9 isslmd.u ⊢1˙=1F
10 isslmd.o ⊢O=0F
11 fvex ⊢Baseg∈V
12 fvex ⊢+g∈V
13 fvex ⊢⋅g∈V
14 fvex ⊢Scalar⁡g∈V
15 fvex ⊢Basef∈V
16 fvex ⊢+f∈V
17 fvex ⊢⋅f∈V
18 simp1 ⊢k=Basef∧p=+f∧t=⋅f→k=Basef
19 simp2 ⊢k=Basef∧p=+f∧t=⋅f→p=+f
20 19 oveqd ⊢k=Basef∧p=+f∧t=⋅f→qpr=q+fr
21 20 oveq1d ⊢k=Basef∧p=+f∧t=⋅f→qprsw=q+frsw
22 21 eqeq1d ⊢k=Basef∧p=+f∧t=⋅f→qprsw=qswarsw↔q+frsw=qswarsw
23 22 3anbi3d ⊢k=Basef∧p=+f∧t=⋅f→rsw∈v∧rswax=rswarsx∧qprsw=qswarsw↔rsw∈v∧rswax=rswarsx∧q+frsw=qswarsw
24 simp3 ⊢k=Basef∧p=+f∧t=⋅f→t=⋅f
25 24 oveqd ⊢k=Basef∧p=+f∧t=⋅f→qtr=q⋅fr
26 25 oveq1d ⊢k=Basef∧p=+f∧t=⋅f→qtrsw=q⋅frsw
27 26 eqeq1d ⊢k=Basef∧p=+f∧t=⋅f→qtrsw=qsrsw↔q⋅frsw=qsrsw
28 27 3anbi1d ⊢k=Basef∧p=+f∧t=⋅f→qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g
29 23 28 anbi12d ⊢k=Basef∧p=+f∧t=⋅f→rsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔rsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g
30 29 2ralbidv ⊢k=Basef∧p=+f∧t=⋅f→∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g
31 18 30 raleqbidv ⊢k=Basef∧p=+f∧t=⋅f→∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔∀r∈Basef∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g
32 18 31 raleqbidv ⊢k=Basef∧p=+f∧t=⋅f→∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔∀q∈Basef∀r∈Basef∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g
33 32 anbi2d ⊢k=Basef∧p=+f∧t=⋅f→f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔f∈SRing∧∀q∈Basef∀r∈Basef∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g
34 15 16 17 33 sbc3ie ⊢[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔f∈SRing∧∀q∈Basef∀r∈Basef∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g
35 simpr ⊢s=⋅g∧f=Scalar⁡g→f=Scalar⁡g
36 35 eleq1d ⊢s=⋅g∧f=Scalar⁡g→f∈SRing↔Scalar⁡g∈SRing
37 35 fveq2d ⊢s=⋅g∧f=Scalar⁡g→Basef=BaseScalar⁡g
38 simpl ⊢s=⋅g∧f=Scalar⁡g→s=⋅g
39 38 oveqd ⊢s=⋅g∧f=Scalar⁡g→rsw=r⋅gw
40 39 eleq1d ⊢s=⋅g∧f=Scalar⁡g→rsw∈v↔r⋅gw∈v
41 38 oveqd ⊢s=⋅g∧f=Scalar⁡g→rswax=r⋅gwax
42 38 oveqd ⊢s=⋅g∧f=Scalar⁡g→rsx=r⋅gx
43 39 42 oveq12d ⊢s=⋅g∧f=Scalar⁡g→rswarsx=r⋅gwar⋅gx
44 41 43 eqeq12d ⊢s=⋅g∧f=Scalar⁡g→rswax=rswarsx↔r⋅gwax=r⋅gwar⋅gx
45 35 fveq2d ⊢s=⋅g∧f=Scalar⁡g→+f=+Scalar⁡g
46 45 oveqd ⊢s=⋅g∧f=Scalar⁡g→q+fr=q+Scalar⁡gr
47 eqidd ⊢s=⋅g∧f=Scalar⁡g→w=w
48 38 46 47 oveq123d ⊢s=⋅g∧f=Scalar⁡g→q+frsw=q+Scalar⁡gr⋅gw
49 38 oveqd ⊢s=⋅g∧f=Scalar⁡g→qsw=q⋅gw
50 49 39 oveq12d ⊢s=⋅g∧f=Scalar⁡g→qswarsw=q⋅gwar⋅gw
51 48 50 eqeq12d ⊢s=⋅g∧f=Scalar⁡g→q+frsw=qswarsw↔q+Scalar⁡gr⋅gw=q⋅gwar⋅gw
52 40 44 51 3anbi123d ⊢s=⋅g∧f=Scalar⁡g→rsw∈v∧rswax=rswarsx∧q+frsw=qswarsw↔r⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw
53 35 fveq2d ⊢s=⋅g∧f=Scalar⁡g→⋅f=⋅Scalar⁡g
54 53 oveqd ⊢s=⋅g∧f=Scalar⁡g→q⋅fr=q⋅Scalar⁡gr
55 38 54 47 oveq123d ⊢s=⋅g∧f=Scalar⁡g→q⋅frsw=q⋅Scalar⁡gr⋅gw
56 eqidd ⊢s=⋅g∧f=Scalar⁡g→q=q
57 38 56 39 oveq123d ⊢s=⋅g∧f=Scalar⁡g→qsrsw=q⋅gr⋅gw
58 55 57 eqeq12d ⊢s=⋅g∧f=Scalar⁡g→q⋅frsw=qsrsw↔q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw
59 35 fveq2d ⊢s=⋅g∧f=Scalar⁡g→1f=1Scalar⁡g
60 38 59 47 oveq123d ⊢s=⋅g∧f=Scalar⁡g→1fsw=1Scalar⁡g⋅gw
61 60 eqeq1d ⊢s=⋅g∧f=Scalar⁡g→1fsw=w↔1Scalar⁡g⋅gw=w
62 35 fveq2d ⊢s=⋅g∧f=Scalar⁡g→0f=0Scalar⁡g
63 38 62 47 oveq123d ⊢s=⋅g∧f=Scalar⁡g→0fsw=0Scalar⁡g⋅gw
64 63 eqeq1d ⊢s=⋅g∧f=Scalar⁡g→0fsw=0g↔0Scalar⁡g⋅gw=0g
65 58 61 64 3anbi123d ⊢s=⋅g∧f=Scalar⁡g→q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g↔q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
66 52 65 anbi12d ⊢s=⋅g∧f=Scalar⁡g→rsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g↔r⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
67 66 2ralbidv ⊢s=⋅g∧f=Scalar⁡g→∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g↔∀x∈v∀w∈vr⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
68 37 67 raleqbidv ⊢s=⋅g∧f=Scalar⁡g→∀r∈Basef∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g↔∀r∈BaseScalar⁡g∀x∈v∀w∈vr⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
69 37 68 raleqbidv ⊢s=⋅g∧f=Scalar⁡g→∀q∈Basef∀r∈Basef∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g↔∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈v∀w∈vr⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
70 36 69 anbi12d ⊢s=⋅g∧f=Scalar⁡g→f∈SRing∧∀q∈Basef∀r∈Basef∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧q+frsw=qswarsw∧q⋅frsw=qsrsw∧1fsw=w∧0fsw=0g↔Scalar⁡g∈SRing∧∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈v∀w∈vr⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
71 34 70 bitrid ⊢s=⋅g∧f=Scalar⁡g→[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔Scalar⁡g∈SRing∧∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈v∀w∈vr⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
72 13 14 71 sbc2ie ⊢[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔Scalar⁡g∈SRing∧∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈v∀w∈vr⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
73 simpl ⊢v=Baseg∧a=+g→v=Baseg
74 73 eleq2d ⊢v=Baseg∧a=+g→r⋅gw∈v↔r⋅gw∈Baseg
75 simpr ⊢v=Baseg∧a=+g→a=+g
76 75 oveqd ⊢v=Baseg∧a=+g→wax=w+gx
77 76 oveq2d ⊢v=Baseg∧a=+g→r⋅gwax=r⋅gw+gx
78 75 oveqd ⊢v=Baseg∧a=+g→r⋅gwar⋅gx=r⋅gw+gr⋅gx
79 77 78 eqeq12d ⊢v=Baseg∧a=+g→r⋅gwax=r⋅gwar⋅gx↔r⋅gw+gx=r⋅gw+gr⋅gx
80 75 oveqd ⊢v=Baseg∧a=+g→q⋅gwar⋅gw=q⋅gw+gr⋅gw
81 80 eqeq2d ⊢v=Baseg∧a=+g→q+Scalar⁡gr⋅gw=q⋅gwar⋅gw↔q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw
82 74 79 81 3anbi123d ⊢v=Baseg∧a=+g→r⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw↔r⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw
83 82 anbi1d ⊢v=Baseg∧a=+g→r⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔r⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
84 73 83 raleqbidv ⊢v=Baseg∧a=+g→∀w∈vr⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
85 73 84 raleqbidv ⊢v=Baseg∧a=+g→∀x∈v∀w∈vr⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔∀x∈Baseg∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
86 85 2ralbidv ⊢v=Baseg∧a=+g→∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈v∀w∈vr⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈Baseg∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
87 86 anbi2d ⊢v=Baseg∧a=+g→Scalar⁡g∈SRing∧∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈v∀w∈vr⋅gw∈v∧r⋅gwax=r⋅gwar⋅gx∧q+Scalar⁡gr⋅gw=q⋅gwar⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔Scalar⁡g∈SRing∧∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈Baseg∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
88 72 87 bitrid ⊢v=Baseg∧a=+g→[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔Scalar⁡g∈SRing∧∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈Baseg∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
89 11 12 88 sbc2ie ⊢[˙Baseg/v]˙[˙+g/a]˙[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔Scalar⁡g∈SRing∧∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈Baseg∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g
90 fveq2 ⊢g=W→Scalar⁡g=Scalar⁡W
91 90 5 eqtr4di ⊢g=W→Scalar⁡g=F
92 91 eleq1d ⊢g=W→Scalar⁡g∈SRing↔F∈SRing
93 91 fveq2d ⊢g=W→BaseScalar⁡g=BaseF
94 93 6 eqtr4di ⊢g=W→BaseScalar⁡g=K
95 fveq2 ⊢g=W→Baseg=BaseW
96 95 1 eqtr4di ⊢g=W→Baseg=V
97 fveq2 ⊢g=W→⋅g=⋅W
98 97 3 eqtr4di ⊢g=W→⋅g=·˙
99 98 oveqd ⊢g=W→r⋅gw=r·˙w
100 99 96 eleq12d ⊢g=W→r⋅gw∈Baseg↔r·˙w∈V
101 eqidd ⊢g=W→r=r
102 fveq2 ⊢g=W→+g=+W
103 102 2 eqtr4di ⊢g=W→+g=+˙
104 103 oveqd ⊢g=W→w+gx=w+˙x
105 98 101 104 oveq123d ⊢g=W→r⋅gw+gx=r·˙w+˙x
106 98 oveqd ⊢g=W→r⋅gx=r·˙x
107 103 99 106 oveq123d ⊢g=W→r⋅gw+gr⋅gx=r·˙w+˙r·˙x
108 105 107 eqeq12d ⊢g=W→r⋅gw+gx=r⋅gw+gr⋅gx↔r·˙w+˙x=r·˙w+˙r·˙x
109 91 fveq2d ⊢g=W→+Scalar⁡g=+F
110 109 7 eqtr4di ⊢g=W→+Scalar⁡g=⨣˙
111 110 oveqd ⊢g=W→q+Scalar⁡gr=q⨣˙r
112 eqidd ⊢g=W→w=w
113 98 111 112 oveq123d ⊢g=W→q+Scalar⁡gr⋅gw=q⨣˙r·˙w
114 98 oveqd ⊢g=W→q⋅gw=q·˙w
115 103 114 99 oveq123d ⊢g=W→q⋅gw+gr⋅gw=q·˙w+˙r·˙w
116 113 115 eqeq12d ⊢g=W→q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw↔q⨣˙r·˙w=q·˙w+˙r·˙w
117 100 108 116 3anbi123d ⊢g=W→r⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw↔r·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w
118 91 fveq2d ⊢g=W→⋅Scalar⁡g=⋅F
119 118 8 eqtr4di ⊢g=W→⋅Scalar⁡g=×˙
120 119 oveqd ⊢g=W→q⋅Scalar⁡gr=q×˙r
121 98 120 112 oveq123d ⊢g=W→q⋅Scalar⁡gr⋅gw=q×˙r·˙w
122 eqidd ⊢g=W→q=q
123 98 122 99 oveq123d ⊢g=W→q⋅gr⋅gw=q·˙r·˙w
124 121 123 eqeq12d ⊢g=W→q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw↔q×˙r·˙w=q·˙r·˙w
125 91 fveq2d ⊢g=W→1Scalar⁡g=1F
126 125 9 eqtr4di ⊢g=W→1Scalar⁡g=1˙
127 98 126 112 oveq123d ⊢g=W→1Scalar⁡g⋅gw=1˙·˙w
128 127 eqeq1d ⊢g=W→1Scalar⁡g⋅gw=w↔1˙·˙w=w
129 91 fveq2d ⊢g=W→0Scalar⁡g=0F
130 129 10 eqtr4di ⊢g=W→0Scalar⁡g=O
131 98 130 112 oveq123d ⊢g=W→0Scalar⁡g⋅gw=O·˙w
132 fveq2 ⊢g=W→0g=0W
133 132 4 eqtr4di ⊢g=W→0g=0˙
134 131 133 eqeq12d ⊢g=W→0Scalar⁡g⋅gw=0g↔O·˙w=0˙
135 124 128 134 3anbi123d ⊢g=W→q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙
136 117 135 anbi12d ⊢g=W→r⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔r·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙
137 96 136 raleqbidv ⊢g=W→∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙
138 96 137 raleqbidv ⊢g=W→∀x∈Baseg∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔∀x∈V∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙
139 94 138 raleqbidv ⊢g=W→∀r∈BaseScalar⁡g∀x∈Baseg∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔∀r∈K∀x∈V∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙
140 94 139 raleqbidv ⊢g=W→∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈Baseg∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔∀q∈K∀r∈K∀x∈V∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙
141 92 140 anbi12d ⊢g=W→Scalar⁡g∈SRing∧∀q∈BaseScalar⁡g∀r∈BaseScalar⁡g∀x∈Baseg∀w∈Basegr⋅gw∈Baseg∧r⋅gw+gx=r⋅gw+gr⋅gx∧q+Scalar⁡gr⋅gw=q⋅gw+gr⋅gw∧q⋅Scalar⁡gr⋅gw=q⋅gr⋅gw∧1Scalar⁡g⋅gw=w∧0Scalar⁡g⋅gw=0g↔F∈SRing∧∀q∈K∀r∈K∀x∈V∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙
142 89 141 bitrid ⊢g=W→[˙Baseg/v]˙[˙+g/a]˙[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g↔F∈SRing∧∀q∈K∀r∈K∀x∈V∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙
143 df-slmd ⊢SLMod=g∈CMnd|[˙Baseg/v]˙[˙+g/a]˙[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
144 142 143 elrab2 ⊢W∈SLMod↔W∈CMnd∧F∈SRing∧∀q∈K∀r∈K∀x∈V∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙
145 3anass ⊢W∈CMnd∧F∈SRing∧∀q∈K∀r∈K∀x∈V∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙↔W∈CMnd∧F∈SRing∧∀q∈K∀r∈K∀x∈V∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙
146 144 145 bitr4i ⊢W∈SLMod↔W∈CMnd∧F∈SRing∧∀q∈K∀r∈K∀x∈V∀w∈Vr·˙w∈V∧r·˙w+˙x=r·˙w+˙r·˙x∧q⨣˙r·˙w=q·˙w+˙r·˙w∧q×˙r·˙w=q·˙r·˙w∧1˙·˙w=w∧O·˙w=0˙