Metamath Proof Explorer


Theorem cramer0

Description: Special case of Cramer's rule for 0-dimensional matrices/vectors. (Contributed by AV, 28-Feb-2019)

Ref Expression
Hypotheses cramer.a A = N Mat R
cramer.b B = Base A
cramer.v V = Base R N
cramer.d D = N maDet R
cramer.x · ˙ = R maVecMul N N
cramer.q × ˙ = / r R
Assertion cramer0 N = R CRing X B Y V D X Unit R Z = i N D X N matRepV R Y i × ˙ D X X · ˙ Z = Y

Proof

Step Hyp Ref Expression
1 cramer.a A = N Mat R
2 cramer.b B = Base A
3 cramer.v V = Base R N
4 cramer.d D = N maDet R
5 cramer.x · ˙ = R maVecMul N N
6 cramer.q × ˙ = / r R
7 1 fveq2i Base A = Base N Mat R
8 2 7 eqtri B = Base N Mat R
9 fvoveq1 N = Base N Mat R = Base Mat R
10 8 9 syl5eq N = B = Base Mat R
11 10 adantr N = R CRing B = Base Mat R
12 11 eleq2d N = R CRing X B X Base Mat R
13 mat0dimbas0 R CRing Base Mat R =
14 13 eleq2d R CRing X Base Mat R X
15 14 adantl N = R CRing X Base Mat R X
16 12 15 bitrd N = R CRing X B X
17 3 a1i N = R CRing V = Base R N
18 oveq2 N = Base R N = Base R
19 18 adantr N = R CRing Base R N = Base R
20 fvex Base R V
21 map0e Base R V Base R = 1 𝑜
22 20 21 mp1i N = R CRing Base R = 1 𝑜
23 17 19 22 3eqtrd N = R CRing V = 1 𝑜
24 23 eleq2d N = R CRing Y V Y 1 𝑜
25 el1o Y 1 𝑜 Y =
26 24 25 bitrdi N = R CRing Y V Y =
27 16 26 anbi12d N = R CRing X B Y V X Y =
28 elsni X X =
29 mpteq1 N = i N D X N matRepV R Y i × ˙ D X = i D X N matRepV R Y i × ˙ D X
30 mpt0 i D X N matRepV R Y i × ˙ D X =
31 29 30 eqtrdi N = i N D X N matRepV R Y i × ˙ D X =
32 31 eqeq2d N = Z = i N D X N matRepV R Y i × ˙ D X Z =
33 32 ad2antrr N = R CRing X = Y = Z = i N D X N matRepV R Y i × ˙ D X Z =
34 simplrl N = R CRing X = Y = Z = X =
35 simpr N = R CRing X = Y = Z = Z =
36 34 35 oveq12d N = R CRing X = Y = Z = X · ˙ Z = · ˙
37 5 mavmul0 N = R CRing · ˙ =
38 37 ad2antrr N = R CRing X = Y = Z = · ˙ =
39 simpr X = Y = Y =
40 39 eqcomd X = Y = = Y
41 40 ad2antlr N = R CRing X = Y = Z = = Y
42 36 38 41 3eqtrd N = R CRing X = Y = Z = X · ˙ Z = Y
43 42 ex N = R CRing X = Y = Z = X · ˙ Z = Y
44 33 43 sylbid N = R CRing X = Y = Z = i N D X N matRepV R Y i × ˙ D X X · ˙ Z = Y
45 44 a1d N = R CRing X = Y = D X Unit R Z = i N D X N matRepV R Y i × ˙ D X X · ˙ Z = Y
46 45 ex N = R CRing X = Y = D X Unit R Z = i N D X N matRepV R Y i × ˙ D X X · ˙ Z = Y
47 28 46 sylani N = R CRing X Y = D X Unit R Z = i N D X N matRepV R Y i × ˙ D X X · ˙ Z = Y
48 27 47 sylbid N = R CRing X B Y V D X Unit R Z = i N D X N matRepV R Y i × ˙ D X X · ˙ Z = Y
49 48 3imp N = R CRing X B Y V D X Unit R Z = i N D X N matRepV R Y i × ˙ D X X · ˙ Z = Y