Metamath Proof Explorer

Theorem matsubgcell

Description: Subtraction in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019)

Ref Expression
Hypotheses matplusgcell.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matplusgcell.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
matsubgcell.s ⊢ 𝑆 = ( -g ‘ 𝐴 )
matsubgcell.m ⊢ − = ( -g ‘ 𝑅 )
Assertion matsubgcell ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 𝑆 𝑌 ) 𝐽 ) = ( ( 𝐼 𝑋 𝐽 ) − ( 𝐼 𝑌 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 matplusgcell.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matplusgcell.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 matsubgcell.s ⊢ 𝑆 = ( -g ‘ 𝐴 )
4 matsubgcell.m ⊢ − = ( -g ‘ 𝑅 )
5 1 2 matrcl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
6 5 simpld ⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
7 6 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑁 ∈ Fin )
8 7 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
9 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
10 eqid ⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
11 1 10 matsubg ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( -g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( -g ‘ 𝐴 ) )
12 8 9 11 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( -g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( -g ‘ 𝐴 ) )
13 3 12 eqtr4id ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑆 = ( -g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
14 13 oveqd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑋 𝑆 𝑌 ) = ( 𝑋 ( -g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑌 ) )
15 eqid ⊢ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
16 xpfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
17 16 anidms ⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ Fin )
18 17 adantr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑁 × 𝑁 ) ∈ Fin )
19 5 18 syl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 × 𝑁 ) ∈ Fin )
20 19 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 × 𝑁 ) ∈ Fin )
21 20 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑁 × 𝑁 ) ∈ Fin )
22 2 eleq2i ⊢ ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ 𝐴 ) )
23 22 biimpi ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
24 1 10 matbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
25 5 24 syl ⊢ ( 𝑋 ∈ 𝐵 → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
26 23 25 eleqtrrd ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
27 26 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
28 27 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑋 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
29 2 eleq2i ⊢ ( 𝑌 ∈ 𝐵 ↔ 𝑌 ∈ ( Base ‘ 𝐴 ) )
30 29 biimpi ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( Base ‘ 𝐴 ) )
31 1 2 matrcl ⊢ ( 𝑌 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
32 31 24 syl ⊢ ( 𝑌 ∈ 𝐵 → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
33 30 32 eleqtrrd ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
34 33 adantl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
35 34 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑌 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
36 eqid ⊢ ( -g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( -g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
37 10 15 9 21 28 35 4 36 frlmsubgval ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑋 ( -g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑌 ) = ( 𝑋 ∘f − 𝑌 ) )
38 14 37 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑋 𝑆 𝑌 ) = ( 𝑋 ∘f − 𝑌 ) )
39 38 oveqd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 𝑆 𝑌 ) 𝐽 ) = ( 𝐼 ( 𝑋 ∘f − 𝑌 ) 𝐽 ) )
40 df-ov ⊢ ( 𝐼 ( 𝑋 ∘f − 𝑌 ) 𝐽 ) = ( ( 𝑋 ∘f − 𝑌 ) ‘ ⟨ 𝐼 , 𝐽 ⟩ )
41 opelxpi ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑁 × 𝑁 ) )
42 41 anim2i ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑁 × 𝑁 ) ) )
43 42 3adant1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑁 × 𝑁 ) ) )
44 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
45 1 44 2 matbas2i ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
46 elmapfn ⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑋 Fn ( 𝑁 × 𝑁 ) )
47 45 46 syl ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 Fn ( 𝑁 × 𝑁 ) )
48 47 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 Fn ( 𝑁 × 𝑁 ) )
49 1 44 2 matbas2i ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
50 elmapfn ⊢ ( 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑌 Fn ( 𝑁 × 𝑁 ) )
51 49 50 syl ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 Fn ( 𝑁 × 𝑁 ) )
52 51 adantl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 Fn ( 𝑁 × 𝑁 ) )
53 inidm ⊢ ( ( 𝑁 × 𝑁 ) ∩ ( 𝑁 × 𝑁 ) ) = ( 𝑁 × 𝑁 )
54 df-ov ⊢ ( 𝐼 𝑋 𝐽 ) = ( 𝑋 ‘ ⟨ 𝐼 , 𝐽 ⟩ )
55 54 eqcomi ⊢ ( 𝑋 ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐼 𝑋 𝐽 )
56 55 a1i ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑁 × 𝑁 ) ) → ( 𝑋 ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐼 𝑋 𝐽 ) )
57 df-ov ⊢ ( 𝐼 𝑌 𝐽 ) = ( 𝑌 ‘ ⟨ 𝐼 , 𝐽 ⟩ )
58 57 eqcomi ⊢ ( 𝑌 ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐼 𝑌 𝐽 )
59 58 a1i ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑁 × 𝑁 ) ) → ( 𝑌 ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐼 𝑌 𝐽 ) )
60 48 52 20 20 53 56 59 ofval ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑁 × 𝑁 ) ) → ( ( 𝑋 ∘f − 𝑌 ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( ( 𝐼 𝑋 𝐽 ) − ( 𝐼 𝑌 𝐽 ) ) )
61 43 60 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 𝑋 ∘f − 𝑌 ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( ( 𝐼 𝑋 𝐽 ) − ( 𝐼 𝑌 𝐽 ) ) )
62 40 61 syl5eq ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 ∘f − 𝑌 ) 𝐽 ) = ( ( 𝐼 𝑋 𝐽 ) − ( 𝐼 𝑌 𝐽 ) ) )
63 39 62 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 𝑆 𝑌 ) 𝐽 ) = ( ( 𝐼 𝑋 𝐽 ) − ( 𝐼 𝑌 𝐽 ) ) )