Metamath Proof Explorer

Theorem scmateALT

Description: Alternate proof of scmate : An entry of an N x N scalar matrix over the ring R . This prove makes use of scmatmats but is longer and requires more distinct variables. (Contributed by AV, 19-Dec-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses scmatmat.a ⊢ A = N Mat R
scmatmat.b ⊢ B = Base A
scmatmat.s ⊢ S = N ScMat R
scmate.k ⊢ K = Base R
scmate.0 ⊢ 0 ˙ = 0 R
Assertion scmateALT ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S ∧ I ∈ N ∧ J ∈ N → ∃ c ∈ K I M J = if I = J c 0 ˙

Proof

Step Hyp Ref Expression
1 scmatmat.a ⊢ A = N Mat R
2 scmatmat.b ⊢ B = Base A
3 scmatmat.s ⊢ S = N ScMat R
4 scmate.k ⊢ K = Base R
5 scmate.0 ⊢ 0 ˙ = 0 R
6 1 2 3 4 5 scmatmats ⊢ N ∈ Fin ∧ R ∈ Ring → S = m ∈ B | ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙
7 6 eleq2d ⊢ N ∈ Fin ∧ R ∈ Ring → M ∈ S ↔ M ∈ m ∈ B | ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙
8 oveq ⊢ m = M → i m j = i M j
9 8 eqeq1d ⊢ m = M → i m j = if i = j c 0 ˙ ↔ i M j = if i = j c 0 ˙
10 9 2ralbidv ⊢ m = M → ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙ ↔ ∀ i ∈ N ∀ j ∈ N i M j = if i = j c 0 ˙
11 10 rexbidv ⊢ m = M → ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙ ↔ ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i M j = if i = j c 0 ˙
12 11 elrab ⊢ M ∈ m ∈ B | ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙ ↔ M ∈ B ∧ ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i M j = if i = j c 0 ˙
13 oveq1 ⊢ i = I → i M j = I M j
14 eqeq1 ⊢ i = I → i = j ↔ I = j
15 14 ifbid ⊢ i = I → if i = j c 0 ˙ = if I = j c 0 ˙
16 13 15 eqeq12d ⊢ i = I → i M j = if i = j c 0 ˙ ↔ I M j = if I = j c 0 ˙
17 oveq2 ⊢ j = J → I M j = I M J
18 eqeq2 ⊢ j = J → I = j ↔ I = J
19 18 ifbid ⊢ j = J → if I = j c 0 ˙ = if I = J c 0 ˙
20 17 19 eqeq12d ⊢ j = J → I M j = if I = j c 0 ˙ ↔ I M J = if I = J c 0 ˙
21 16 20 rspc2v ⊢ I ∈ N ∧ J ∈ N → ∀ i ∈ N ∀ j ∈ N i M j = if i = j c 0 ˙ → I M J = if I = J c 0 ˙
22 21 reximdv ⊢ I ∈ N ∧ J ∈ N → ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i M j = if i = j c 0 ˙ → ∃ c ∈ K I M J = if I = J c 0 ˙
23 22 com12 ⊢ ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i M j = if i = j c 0 ˙ → I ∈ N ∧ J ∈ N → ∃ c ∈ K I M J = if I = J c 0 ˙
24 23 adantl ⊢ M ∈ B ∧ ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i M j = if i = j c 0 ˙ → I ∈ N ∧ J ∈ N → ∃ c ∈ K I M J = if I = J c 0 ˙
25 24 a1i ⊢ N ∈ Fin ∧ R ∈ Ring → M ∈ B ∧ ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i M j = if i = j c 0 ˙ → I ∈ N ∧ J ∈ N → ∃ c ∈ K I M J = if I = J c 0 ˙
26 12 25 biimtrid ⊢ N ∈ Fin ∧ R ∈ Ring → M ∈ m ∈ B | ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙ → I ∈ N ∧ J ∈ N → ∃ c ∈ K I M J = if I = J c 0 ˙
27 7 26 sylbid ⊢ N ∈ Fin ∧ R ∈ Ring → M ∈ S → I ∈ N ∧ J ∈ N → ∃ c ∈ K I M J = if I = J c 0 ˙
28 27 ex ⊢ N ∈ Fin → R ∈ Ring → M ∈ S → I ∈ N ∧ J ∈ N → ∃ c ∈ K I M J = if I = J c 0 ˙
29 28 3imp1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S ∧ I ∈ N ∧ J ∈ N → ∃ c ∈ K I M J = if I = J c 0 ˙