Metamath Proof Explorer


Theorem mat1dimscm

Description: The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019)

Ref Expression
Hypotheses mat1dim.a A = E Mat R
mat1dim.b B = Base R
mat1dim.o O = E E
Assertion mat1dimscm R Ring E V X B Y B X A O Y = O X R Y

Proof

Step Hyp Ref Expression
1 mat1dim.a A = E Mat R
2 mat1dim.b B = Base R
3 mat1dim.o O = E E
4 opex E E V
5 3 4 eqeltri O V
6 5 a1i Y B O V
7 6 anim2i X B Y B X B O V
8 7 ancomd X B Y B O V X B
9 fnsng O V X B O X Fn O
10 8 9 syl X B Y B O X Fn O
11 10 adantl R Ring E V X B Y B O X Fn O
12 xpsng O V X B O × X = O X
13 8 12 syl X B Y B O × X = O X
14 13 adantl R Ring E V X B Y B O × X = O X
15 14 fneq1d R Ring E V X B Y B O × X Fn O O X Fn O
16 11 15 mpbird R Ring E V X B Y B O × X Fn O
17 xpsng E V E V E × E = E E
18 3 sneqi O = E E
19 17 18 syl6eqr E V E V E × E = O
20 19 anidms E V E × E = O
21 20 ad2antlr R Ring E V X B Y B E × E = O
22 21 xpeq1d R Ring E V X B Y B E × E × X = O × X
23 22 fneq1d R Ring E V X B Y B E × E × X Fn O O × X Fn O
24 16 23 mpbird R Ring E V X B Y B E × E × X Fn O
25 5 a1i X B O V
26 fnsng O V Y B O Y Fn O
27 25 26 sylan X B Y B O Y Fn O
28 27 adantl R Ring E V X B Y B O Y Fn O
29 snex O V
30 29 a1i R Ring E V X B Y B O V
31 inidm O O = O
32 elsni x O x = O
33 fveq2 x = O E × E × X x = E × E × X O
34 17 anidms E V E × E = E E
35 34 ad2antlr R Ring E V X B Y B E × E = E E
36 35 xpeq1d R Ring E V X B Y B E × E × X = E E × X
37 4 a1i Y B E E V
38 37 anim2i X B Y B X B E E V
39 38 ancomd X B Y B E E V X B
40 xpsng E E V X B E E × X = E E X
41 3 eqcomi E E = O
42 41 opeq1i E E X = O X
43 42 sneqi E E X = O X
44 40 43 syl6eq E E V X B E E × X = O X
45 39 44 syl X B Y B E E × X = O X
46 45 adantl R Ring E V X B Y B E E × X = O X
47 36 46 eqtrd R Ring E V X B Y B E × E × X = O X
48 47 fveq1d R Ring E V X B Y B E × E × X O = O X O
49 fvsng O V X B O X O = X
50 8 49 syl X B Y B O X O = X
51 50 adantl R Ring E V X B Y B O X O = X
52 48 51 eqtrd R Ring E V X B Y B E × E × X O = X
53 33 52 sylan9eq x = O R Ring E V X B Y B E × E × X x = X
54 53 ex x = O R Ring E V X B Y B E × E × X x = X
55 32 54 syl x O R Ring E V X B Y B E × E × X x = X
56 55 impcom R Ring E V X B Y B x O E × E × X x = X
57 fveq2 x = O O Y x = O Y O
58 fvsng O V Y B O Y O = Y
59 25 58 sylan X B Y B O Y O = Y
60 59 adantl R Ring E V X B Y B O Y O = Y
61 57 60 sylan9eq x = O R Ring E V X B Y B O Y x = Y
62 61 ex x = O R Ring E V X B Y B O Y x = Y
63 32 62 syl x O R Ring E V X B Y B O Y x = Y
64 63 impcom R Ring E V X B Y B x O O Y x = Y
65 24 28 30 30 31 56 64 offval R Ring E V X B Y B E × E × X R f O Y = x O X R Y
66 simprl R Ring E V X B Y B X B
67 simpr X B Y B Y B
68 67 anim2i R Ring E V X B Y B R Ring E V Y B
69 df-3an R Ring E V Y B R Ring E V Y B
70 68 69 sylibr R Ring E V X B Y B R Ring E V Y B
71 1 2 3 mat1dimbas R Ring E V Y B O Y Base A
72 70 71 syl R Ring E V X B Y B O Y Base A
73 eqid Base A = Base A
74 eqid A = A
75 eqid R = R
76 eqid E × E = E × E
77 1 73 2 74 75 76 matvsca2 X B O Y Base A X A O Y = E × E × X R f O Y
78 66 72 77 syl2anc R Ring E V X B Y B X A O Y = E × E × X R f O Y
79 3anass R Ring X B Y B R Ring X B Y B
80 79 biimpri R Ring X B Y B R Ring X B Y B
81 80 adantlr R Ring E V X B Y B R Ring X B Y B
82 2 75 ringcl R Ring X B Y B X R Y B
83 81 82 syl R Ring E V X B Y B X R Y B
84 fmptsn O V X R Y B O X R Y = x O X R Y
85 5 83 84 sylancr R Ring E V X B Y B O X R Y = x O X R Y
86 65 78 85 3eqtr4d R Ring E V X B Y B X A O Y = O X R Y