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 𝐴 = ( 𝑁 Mat 𝑅 )
cramer.b 𝐵 = ( Base ‘ 𝐴 )
cramer.v 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
cramer.d 𝐷 = ( 𝑁 maDet 𝑅 )
cramer.x · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
cramer.q / = ( /r𝑅 )
Assertion cramer0 ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝐷𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑍 = ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 cramer.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 cramer.b 𝐵 = ( Base ‘ 𝐴 )
3 cramer.v 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4 cramer.d 𝐷 = ( 𝑁 maDet 𝑅 )
5 cramer.x · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
6 cramer.q / = ( /r𝑅 )
7 1 fveq2i ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
8 2 7 eqtri 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
9 fvoveq1 ( 𝑁 = ∅ → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( ∅ Mat 𝑅 ) ) )
10 8 9 syl5eq ( 𝑁 = ∅ → 𝐵 = ( Base ‘ ( ∅ Mat 𝑅 ) ) )
11 10 adantr ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → 𝐵 = ( Base ‘ ( ∅ Mat 𝑅 ) ) )
12 11 eleq2d ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( 𝑋𝐵𝑋 ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) ) )
13 mat0dimbas0 ( 𝑅 ∈ CRing → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
14 13 eleq2d ( 𝑅 ∈ CRing → ( 𝑋 ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) ↔ 𝑋 ∈ { ∅ } ) )
15 14 adantl ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( 𝑋 ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) ↔ 𝑋 ∈ { ∅ } ) )
16 12 15 bitrd ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( 𝑋𝐵𝑋 ∈ { ∅ } ) )
17 3 a1i ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
18 oveq2 ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = ( ( Base ‘ 𝑅 ) ↑m ∅ ) )
19 18 adantr ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = ( ( Base ‘ 𝑅 ) ↑m ∅ ) )
20 fvex ( Base ‘ 𝑅 ) ∈ V
21 map0e ( ( Base ‘ 𝑅 ) ∈ V → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
22 20 21 mp1i ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
23 17 19 22 3eqtrd ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → 𝑉 = 1o )
24 23 eleq2d ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( 𝑌𝑉𝑌 ∈ 1o ) )
25 el1o ( 𝑌 ∈ 1o𝑌 = ∅ )
26 24 25 bitrdi ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( 𝑌𝑉𝑌 = ∅ ) )
27 16 26 anbi12d ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( ( 𝑋𝐵𝑌𝑉 ) ↔ ( 𝑋 ∈ { ∅ } ∧ 𝑌 = ∅ ) ) )
28 elsni ( 𝑋 ∈ { ∅ } → 𝑋 = ∅ )
29 mpteq1 ( 𝑁 = ∅ → ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) = ( 𝑖 ∈ ∅ ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) )
30 mpt0 ( 𝑖 ∈ ∅ ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) = ∅
31 29 30 eqtrdi ( 𝑁 = ∅ → ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) = ∅ )
32 31 eqeq2d ( 𝑁 = ∅ → ( 𝑍 = ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) ↔ 𝑍 = ∅ ) )
33 32 ad2antrr ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ) → ( 𝑍 = ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) ↔ 𝑍 = ∅ ) )
34 simplrl ( ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ) ∧ 𝑍 = ∅ ) → 𝑋 = ∅ )
35 simpr ( ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ) ∧ 𝑍 = ∅ ) → 𝑍 = ∅ )
36 34 35 oveq12d ( ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ) ∧ 𝑍 = ∅ ) → ( 𝑋 · 𝑍 ) = ( ∅ · ∅ ) )
37 5 mavmul0 ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( ∅ · ∅ ) = ∅ )
38 37 ad2antrr ( ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ) ∧ 𝑍 = ∅ ) → ( ∅ · ∅ ) = ∅ )
39 simpr ( ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) → 𝑌 = ∅ )
40 39 eqcomd ( ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) → ∅ = 𝑌 )
41 40 ad2antlr ( ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ) ∧ 𝑍 = ∅ ) → ∅ = 𝑌 )
42 36 38 41 3eqtrd ( ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ) ∧ 𝑍 = ∅ ) → ( 𝑋 · 𝑍 ) = 𝑌 )
43 42 ex ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ) → ( 𝑍 = ∅ → ( 𝑋 · 𝑍 ) = 𝑌 ) )
44 33 43 sylbid ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ) → ( 𝑍 = ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) )
45 44 a1d ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ) → ( ( 𝐷𝑋 ) ∈ ( Unit ‘ 𝑅 ) → ( 𝑍 = ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) ) )
46 45 ex ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) → ( ( 𝐷𝑋 ) ∈ ( Unit ‘ 𝑅 ) → ( 𝑍 = ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) ) ) )
47 28 46 sylani ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( ( 𝑋 ∈ { ∅ } ∧ 𝑌 = ∅ ) → ( ( 𝐷𝑋 ) ∈ ( Unit ‘ 𝑅 ) → ( 𝑍 = ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) ) ) )
48 27 47 sylbid ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) → ( ( 𝑋𝐵𝑌𝑉 ) → ( ( 𝐷𝑋 ) ∈ ( Unit ‘ 𝑅 ) → ( 𝑍 = ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) ) ) )
49 48 3imp ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝐷𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑍 = ( 𝑖𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) )