Theorem cramerlem1

Description: Lemma 1 for cramer . (Contributed by AV, 21-Feb-2019) (Revised by AV, 1-Mar-2019)

	Ref	Expression
Hypotheses	cramer.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cramer.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cramer.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
	cramer.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	cramer.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
	cramer.q	⊢ / = ( /r ‘ 𝑅 )
Assertion	cramerlem1	⊢ ( ( 𝑅 ∈ 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		simp1	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑅 ∈ CRing )
8	7	anim1i	⊢ ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑅 ∈ CRing ∧ 𝑎 ∈ 𝑁 ) )
9		simpl2	⊢ ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) )
10		pm3.22	⊢ ( ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) )
11	10	3adant2	⊢ ( ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) )
12	11	3ad2ant3	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) )
13	12	adantr	⊢ ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) )
14		eqid	⊢ ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝑎 ) = ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝑎 )
15		eqid	⊢ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑎 ) = ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑎 )
16	1 2 3 14 15 5 4 6	cramerimp	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑎 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑍 ‘ 𝑎 ) = ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑎 ) ) / ( 𝐷 ‘ 𝑋 ) ) )
17	8 9 13 16	syl3anc	⊢ ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑍 ‘ 𝑎 ) = ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑎 ) ) / ( 𝐷 ‘ 𝑋 ) ) )
18	17	ralrimiva	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ∀ 𝑎 ∈ 𝑁 ( 𝑍 ‘ 𝑎 ) = ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑎 ) ) / ( 𝐷 ‘ 𝑋 ) ) )
19		elmapfn	⊢ ( 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) → 𝑍 Fn 𝑁 )
20	19 3	eleq2s	⊢ ( 𝑍 ∈ 𝑉 → 𝑍 Fn 𝑁 )
21	20	3ad2ant2	⊢ ( ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍 Fn 𝑁 )
22	21	3ad2ant3	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑍 Fn 𝑁 )
23		2fveq3	⊢ ( 𝑎 = 𝑖 → ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑎 ) ) = ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) )
24	23	oveq1d	⊢ ( 𝑎 = 𝑖 → ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑎 ) ) / ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) )
25		ovexd	⊢ ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑎 ) ) / ( 𝐷 ‘ 𝑋 ) ) ∈ V )
26		ovexd	⊢ ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ∈ V )
27	22 24 25 26	fnmptfvd	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ↔ ∀ 𝑎 ∈ 𝑁 ( 𝑍 ‘ 𝑎 ) = ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑎 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) )
28	18 27	mpbird	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) )