Metamath Proof Explorer

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 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) )