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	eqtrid	⊢ ( 𝑁 = ∅ → 𝐵 = ( 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 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) )