Metamath Proof Explorer


Theorem rmodislmodlem

Description: Lemma for rmodislmod . This is the part of the proof of rmodislmod which requires the scalar ring to be commutative. (Contributed by AV, 3-Dec-2021)

Ref Expression
Hypotheses rmodislmod.v V = Base R
rmodislmod.a + ˙ = + R
rmodislmod.s · ˙ = R
rmodislmod.f F = Scalar R
rmodislmod.k K = Base F
rmodislmod.p ˙ = + F
rmodislmod.t × ˙ = F
rmodislmod.u 1 ˙ = 1 F
rmodislmod.r R Grp F Ring q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w
rmodislmod.m ˙ = s K , v V v · ˙ s
rmodislmod.l L = R sSet ndx ˙
Assertion rmodislmodlem F CRing a K b K c V a × ˙ b ˙ c = a ˙ b ˙ c

Proof

Step Hyp Ref Expression
1 rmodislmod.v V = Base R
2 rmodislmod.a + ˙ = + R
3 rmodislmod.s · ˙ = R
4 rmodislmod.f F = Scalar R
5 rmodislmod.k K = Base F
6 rmodislmod.p ˙ = + F
7 rmodislmod.t × ˙ = F
8 rmodislmod.u 1 ˙ = 1 F
9 rmodislmod.r R Grp F Ring q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w
10 rmodislmod.m ˙ = s K , v V v · ˙ s
11 rmodislmod.l L = R sSet ndx ˙
12 simprl w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w w · ˙ q × ˙ r = w · ˙ q · ˙ r
13 12 2ralimi x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w x V w V w · ˙ q × ˙ r = w · ˙ q · ˙ r
14 13 2ralimi q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w q K r K x V w V w · ˙ q × ˙ r = w · ˙ q · ˙ r
15 ralrot3 q K r K x V w V w · ˙ q × ˙ r = w · ˙ q · ˙ r x V q K r K w V w · ˙ q × ˙ r = w · ˙ q · ˙ r
16 1 grpbn0 R Grp V
17 16 3ad2ant1 R Grp F Ring q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w V
18 9 17 ax-mp V
19 rspn0 V x V q K r K w V w · ˙ q × ˙ r = w · ˙ q · ˙ r q K r K w V w · ˙ q × ˙ r = w · ˙ q · ˙ r
20 18 19 ax-mp x V q K r K w V w · ˙ q × ˙ r = w · ˙ q · ˙ r q K r K w V w · ˙ q × ˙ r = w · ˙ q · ˙ r
21 oveq1 q = b q × ˙ r = b × ˙ r
22 21 oveq2d q = b w · ˙ q × ˙ r = w · ˙ b × ˙ r
23 oveq2 q = b w · ˙ q = w · ˙ b
24 23 oveq1d q = b w · ˙ q · ˙ r = w · ˙ b · ˙ r
25 22 24 eqeq12d q = b w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ b × ˙ r = w · ˙ b · ˙ r
26 oveq2 r = a b × ˙ r = b × ˙ a
27 26 oveq2d r = a w · ˙ b × ˙ r = w · ˙ b × ˙ a
28 oveq2 r = a w · ˙ b · ˙ r = w · ˙ b · ˙ a
29 27 28 eqeq12d r = a w · ˙ b × ˙ r = w · ˙ b · ˙ r w · ˙ b × ˙ a = w · ˙ b · ˙ a
30 oveq1 w = c w · ˙ b × ˙ a = c · ˙ b × ˙ a
31 oveq1 w = c w · ˙ b = c · ˙ b
32 31 oveq1d w = c w · ˙ b · ˙ a = c · ˙ b · ˙ a
33 30 32 eqeq12d w = c w · ˙ b × ˙ a = w · ˙ b · ˙ a c · ˙ b × ˙ a = c · ˙ b · ˙ a
34 25 29 33 rspc3v b K a K c V q K r K w V w · ˙ q × ˙ r = w · ˙ q · ˙ r c · ˙ b × ˙ a = c · ˙ b · ˙ a
35 34 3com12 a K b K c V q K r K w V w · ˙ q × ˙ r = w · ˙ q · ˙ r c · ˙ b × ˙ a = c · ˙ b · ˙ a
36 20 35 syl5com x V q K r K w V w · ˙ q × ˙ r = w · ˙ q · ˙ r a K b K c V c · ˙ b × ˙ a = c · ˙ b · ˙ a
37 15 36 sylbi q K r K x V w V w · ˙ q × ˙ r = w · ˙ q · ˙ r a K b K c V c · ˙ b × ˙ a = c · ˙ b · ˙ a
38 eqcom c · ˙ b · ˙ a = c · ˙ b × ˙ a c · ˙ b × ˙ a = c · ˙ b · ˙ a
39 37 38 syl6ibr q K r K x V w V w · ˙ q × ˙ r = w · ˙ q · ˙ r a K b K c V c · ˙ b · ˙ a = c · ˙ b × ˙ a
40 14 39 syl q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w a K b K c V c · ˙ b · ˙ a = c · ˙ b × ˙ a
41 40 3ad2ant3 R Grp F Ring q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w a K b K c V c · ˙ b · ˙ a = c · ˙ b × ˙ a
42 9 41 ax-mp a K b K c V c · ˙ b · ˙ a = c · ˙ b × ˙ a
43 42 adantl F CRing a K b K c V c · ˙ b · ˙ a = c · ˙ b × ˙ a
44 5 7 crngcom F CRing b K a K b × ˙ a = a × ˙ b
45 44 3expb F CRing b K a K b × ˙ a = a × ˙ b
46 45 expcom b K a K F CRing b × ˙ a = a × ˙ b
47 46 ancoms a K b K F CRing b × ˙ a = a × ˙ b
48 47 3adant3 a K b K c V F CRing b × ˙ a = a × ˙ b
49 48 impcom F CRing a K b K c V b × ˙ a = a × ˙ b
50 49 oveq2d F CRing a K b K c V c · ˙ b × ˙ a = c · ˙ a × ˙ b
51 43 50 eqtrd F CRing a K b K c V c · ˙ b · ˙ a = c · ˙ a × ˙ b
52 10 a1i a K b K c V ˙ = s K , v V v · ˙ s
53 oveq12 v = c s = b v · ˙ s = c · ˙ b
54 53 ancoms s = b v = c v · ˙ s = c · ˙ b
55 54 adantl a K b K c V s = b v = c v · ˙ s = c · ˙ b
56 simp2 a K b K c V b K
57 simp3 a K b K c V c V
58 ovexd a K b K c V c · ˙ b V
59 52 55 56 57 58 ovmpod a K b K c V b ˙ c = c · ˙ b
60 59 oveq2d a K b K c V a ˙ b ˙ c = a ˙ c · ˙ b
61 oveq12 v = c · ˙ b s = a v · ˙ s = c · ˙ b · ˙ a
62 61 ancoms s = a v = c · ˙ b v · ˙ s = c · ˙ b · ˙ a
63 62 adantl a K b K c V s = a v = c · ˙ b v · ˙ s = c · ˙ b · ˙ a
64 simp1 a K b K c V a K
65 simpl1 w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w w · ˙ r V
66 65 2ralimi x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w x V w V w · ˙ r V
67 66 2ralimi q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w q K r K x V w V w · ˙ r V
68 ringgrp F Ring F Grp
69 5 grpbn0 F Grp K
70 68 69 syl F Ring K
71 70 3ad2ant2 R Grp F Ring q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w K
72 9 71 ax-mp K
73 rspn0 K q K r K x V w V w · ˙ r V r K x V w V w · ˙ r V
74 72 73 ax-mp q K r K x V w V w · ˙ r V r K x V w V w · ˙ r V
75 ralcom r K x V w V w · ˙ r V x V r K w V w · ˙ r V
76 rspn0 V x V r K w V w · ˙ r V r K w V w · ˙ r V
77 18 76 ax-mp x V r K w V w · ˙ r V r K w V w · ˙ r V
78 oveq2 r = b w · ˙ r = w · ˙ b
79 78 eleq1d r = b w · ˙ r V w · ˙ b V
80 31 eleq1d w = c w · ˙ b V c · ˙ b V
81 79 80 rspc2v b K c V r K w V w · ˙ r V c · ˙ b V
82 77 81 syl5com x V r K w V w · ˙ r V b K c V c · ˙ b V
83 75 82 sylbi r K x V w V w · ˙ r V b K c V c · ˙ b V
84 67 74 83 3syl q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w b K c V c · ˙ b V
85 84 3ad2ant3 R Grp F Ring q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w b K c V c · ˙ b V
86 9 85 ax-mp b K c V c · ˙ b V
87 86 3adant1 a K b K c V c · ˙ b V
88 ovexd a K b K c V c · ˙ b · ˙ a V
89 52 63 64 87 88 ovmpod a K b K c V a ˙ c · ˙ b = c · ˙ b · ˙ a
90 60 89 eqtrd a K b K c V a ˙ b ˙ c = c · ˙ b · ˙ a
91 90 adantl F CRing a K b K c V a ˙ b ˙ c = c · ˙ b · ˙ a
92 oveq12 v = c s = a × ˙ b v · ˙ s = c · ˙ a × ˙ b
93 92 ancoms s = a × ˙ b v = c v · ˙ s = c · ˙ a × ˙ b
94 93 adantl a K b K c V s = a × ˙ b v = c v · ˙ s = c · ˙ a × ˙ b
95 5 7 ringcl F Ring a K b K a × ˙ b K
96 95 3expib F Ring a K b K a × ˙ b K
97 96 3ad2ant2 R Grp F Ring q K r K x V w V w · ˙ r V w + ˙ x · ˙ r = w · ˙ r + ˙ x · ˙ r w · ˙ q ˙ r = w · ˙ q + ˙ w · ˙ r w · ˙ q × ˙ r = w · ˙ q · ˙ r w · ˙ 1 ˙ = w a K b K a × ˙ b K
98 9 97 ax-mp a K b K a × ˙ b K
99 98 3adant3 a K b K c V a × ˙ b K
100 ovexd a K b K c V c · ˙ a × ˙ b V
101 52 94 99 57 100 ovmpod a K b K c V a × ˙ b ˙ c = c · ˙ a × ˙ b
102 101 adantl F CRing a K b K c V a × ˙ b ˙ c = c · ˙ a × ˙ b
103 51 91 102 3eqtr4rd F CRing a K b K c V a × ˙ b ˙ c = a ˙ b ˙ c