Metamath Proof Explorer

Theorem cramerlem2

Description: Lemma 2 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 cramerlem2 ( ( 𝑅 ∈ 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 simpll1 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑧 ) = 𝑌 ) → 𝑅 ∈ CRing )
8 simpll2 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑧 ) = 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) )
9 simpll3 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑧 ) = 𝑌 ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) )
10 simplr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑧 ) = 𝑌 ) → 𝑧 ∈ 𝑉 )
11 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑧 ) = 𝑌 ) → ( 𝑋 · 𝑧 ) = 𝑌 )
12 1 2 3 4 5 6 cramerlem1 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝑋 · 𝑧 ) = 𝑌 ) ) → 𝑧 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) )
13 7 8 9 10 11 12 syl113anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑧 ) = 𝑌 ) → 𝑧 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) )
14 13 ex ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑋 · 𝑧 ) = 𝑌 → 𝑧 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) )
15 14 ralrimiva ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ∀ 𝑧 ∈ 𝑉 ( ( 𝑋 · 𝑧 ) = 𝑌 → 𝑧 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) )