Metamath Proof Explorer

Theorem cramerlem3

Description: Lemma 3 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 cramerlem3 ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ 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 2 3 5 4 slesolex ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ∃ 𝑣 ∈ 𝑉 ( 𝑋 · 𝑣 ) = 𝑌 )
8 1 2 3 4 5 6 cramerlem2 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ∀ 𝑧 ∈ 𝑉 ( ( 𝑋 · 𝑧 ) = 𝑌 → 𝑧 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) )
9 8 3adant1l ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ∀ 𝑧 ∈ 𝑉 ( ( 𝑋 · 𝑧 ) = 𝑌 → 𝑧 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) )
10 oveq2 ⊢ ( 𝑧 = 𝑣 → ( 𝑋 · 𝑧 ) = ( 𝑋 · 𝑣 ) )
11 10 eqeq1d ⊢ ( 𝑧 = 𝑣 → ( ( 𝑋 · 𝑧 ) = 𝑌 ↔ ( 𝑋 · 𝑣 ) = 𝑌 ) )
12 oveq2 ⊢ ( 𝑣 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑣 ) = ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) )
13 12 eqeq1d ⊢ ( 𝑣 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( ( 𝑋 · 𝑣 ) = 𝑌 ↔ ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) = 𝑌 ) )
14 11 13 rexraleqim ⊢ ( ( ∃ 𝑣 ∈ 𝑉 ( 𝑋 · 𝑣 ) = 𝑌 ∧ ∀ 𝑧 ∈ 𝑉 ( ( 𝑋 · 𝑧 ) = 𝑌 → 𝑧 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) ) → ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) = 𝑌 )
15 oveq2 ⊢ ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) )
16 15 adantl ⊢ ( ( ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) = 𝑌 ∧ 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) → ( 𝑋 · 𝑍 ) = ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) )
17 simpl ⊢ ( ( ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) = 𝑌 ∧ 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) → ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) = 𝑌 )
18 16 17 eqtrd ⊢ ( ( ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) = 𝑌 ∧ 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 )
19 18 ex ⊢ ( ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) = 𝑌 → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) )
20 19 a1d ⊢ ( ( 𝑋 · ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) = 𝑌 → ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) ) )
21 14 20 syl ⊢ ( ( ∃ 𝑣 ∈ 𝑉 ( 𝑋 · 𝑣 ) = 𝑌 ∧ ∀ 𝑧 ∈ 𝑉 ( ( 𝑋 · 𝑧 ) = 𝑌 → 𝑧 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) ) → ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) ) )
22 21 expcom ⊢ ( ∀ 𝑧 ∈ 𝑉 ( ( 𝑋 · 𝑧 ) = 𝑌 → 𝑧 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) → ( ∃ 𝑣 ∈ 𝑉 ( 𝑋 · 𝑣 ) = 𝑌 → ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) ) ) )
23 22 com23 ⊢ ( ∀ 𝑧 ∈ 𝑉 ( ( 𝑋 · 𝑧 ) = 𝑌 → 𝑧 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) → ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ∃ 𝑣 ∈ 𝑉 ( 𝑋 · 𝑣 ) = 𝑌 → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) ) ) )
24 9 23 mpcom ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ∃ 𝑣 ∈ 𝑉 ( 𝑋 · 𝑣 ) = 𝑌 → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) ) )
25 7 24 mpd ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) )