Metamath Proof Explorer

Theorem mat1scmat

Description: A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat , also a diagonal matrix). (Contributed by AV, 21-Dec-2019)

Ref Expression
Hypotheses mat1scmat.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mat1scmat.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion mat1scmat ( ( 𝑁 ∈ 𝑉 ∧ ( ♯ ‘ 𝑁 ) = 1 ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( 𝑁 ScMat 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 mat1scmat.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mat1scmat.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 hash1snb ⊢ ( 𝑁 ∈ 𝑉 → ( ( ♯ ‘ 𝑁 ) = 1 ↔ ∃ 𝑒 𝑁 = { 𝑒 } ) )
4 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) ) → 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) )
5 eqid ⊢ ( { 𝑒 } Mat 𝑅 ) = ( { 𝑒 } Mat 𝑅 )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ ⟨ 𝑒 , 𝑒 ⟩ = ⟨ 𝑒 , 𝑒 ⟩
8 5 6 7 mat1dimelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑒 ∈ V ) → ( 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) ↔ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑀 = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } ) )
9 8 elvd ⊢ ( 𝑅 ∈ Ring → ( 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) ↔ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑀 = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } ) )
10 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑀 = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } ) → 𝑀 = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } )
11 vex ⊢ 𝑒 ∈ V
12 11 a1i ⊢ ( 𝑐 ∈ ( Base ‘ 𝑅 ) → 𝑒 ∈ V )
13 5 6 7 mat1dimid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑒 ∈ V ) → ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , ( 1r ‘ 𝑅 ) ⟩ } )
14 12 13 sylan2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , ( 1r ‘ 𝑅 ) ⟩ } )
15 14 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) ) = ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , ( 1r ‘ 𝑅 ) ⟩ } ) )
16 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
17 16 11 jctir ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 ∈ Ring ∧ 𝑒 ∈ V ) )
18 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → 𝑐 ∈ ( Base ‘ 𝑅 ) )
19 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20 6 19 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
21 20 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
22 5 6 7 mat1dimscm ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑒 ∈ V ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , ( 1r ‘ 𝑅 ) ⟩ } ) = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , ( 𝑐 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ⟩ } )
23 17 18 21 22 syl12anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , ( 1r ‘ 𝑅 ) ⟩ } ) = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , ( 𝑐 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ⟩ } )
24 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
25 6 24 19 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑐 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑐 )
26 25 opeq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ⟨ ⟨ 𝑒 , 𝑒 ⟩ , ( 𝑐 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ⟩ = ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ )
27 26 sneqd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , ( 𝑐 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ⟩ } = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } )
28 15 23 27 3eqtrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } = ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) ) )
29 28 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑀 = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } ) → { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } = ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) ) )
30 10 29 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑀 = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } ) → 𝑀 = ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) ) )
31 30 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑀 = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } → 𝑀 = ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) ) ) )
32 31 reximdva ⊢ ( 𝑅 ∈ Ring → ( ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑀 = { ⟨ ⟨ 𝑒 , 𝑒 ⟩ , 𝑐 ⟩ } → ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑀 = ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) ) ) )
33 9 32 sylbid ⊢ ( 𝑅 ∈ Ring → ( 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) → ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑀 = ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) ) ) )
34 33 imp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) ) → ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑀 = ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) ) )
35 snfi ⊢ { 𝑒 } ∈ Fin
36 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) ) → 𝑅 ∈ Ring )
37 eqid ⊢ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) = ( Base ‘ ( { 𝑒 } Mat 𝑅 ) )
38 eqid ⊢ ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) = ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) )
39 eqid ⊢ ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) = ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) )
40 eqid ⊢ ( { 𝑒 } ScMat 𝑅 ) = ( { 𝑒 } ScMat 𝑅 )
41 6 5 37 38 39 40 scmatel ⊢ ( ( { 𝑒 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ ( { 𝑒 } ScMat 𝑅 ) ↔ ( 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑀 = ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) ) ) ) )
42 35 36 41 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) ) → ( 𝑀 ∈ ( { 𝑒 } ScMat 𝑅 ) ↔ ( 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑀 = ( 𝑐 ( ·𝑠 ‘ ( { 𝑒 } Mat 𝑅 ) ) ( 1r ‘ ( { 𝑒 } Mat 𝑅 ) ) ) ) ) )
43 4 34 42 mpbir2and ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) ) → 𝑀 ∈ ( { 𝑒 } ScMat 𝑅 ) )
44 43 ex ⊢ ( 𝑅 ∈ Ring → ( 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) → 𝑀 ∈ ( { 𝑒 } ScMat 𝑅 ) ) )
45 1 fveq2i ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
46 2 45 eqtri ⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
47 fvoveq1 ⊢ ( 𝑁 = { 𝑒 } → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) )
48 46 47 eqtrid ⊢ ( 𝑁 = { 𝑒 } → 𝐵 = ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) )
49 48 eleq2d ⊢ ( 𝑁 = { 𝑒 } → ( 𝑀 ∈ 𝐵 ↔ 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) ) )
50 oveq1 ⊢ ( 𝑁 = { 𝑒 } → ( 𝑁 ScMat 𝑅 ) = ( { 𝑒 } ScMat 𝑅 ) )
51 50 eleq2d ⊢ ( 𝑁 = { 𝑒 } → ( 𝑀 ∈ ( 𝑁 ScMat 𝑅 ) ↔ 𝑀 ∈ ( { 𝑒 } ScMat 𝑅 ) ) )
52 49 51 imbi12d ⊢ ( 𝑁 = { 𝑒 } → ( ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( 𝑁 ScMat 𝑅 ) ) ↔ ( 𝑀 ∈ ( Base ‘ ( { 𝑒 } Mat 𝑅 ) ) → 𝑀 ∈ ( { 𝑒 } ScMat 𝑅 ) ) ) )
53 44 52 imbitrrid ⊢ ( 𝑁 = { 𝑒 } → ( 𝑅 ∈ Ring → ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( 𝑁 ScMat 𝑅 ) ) ) )
54 53 exlimiv ⊢ ( ∃ 𝑒 𝑁 = { 𝑒 } → ( 𝑅 ∈ Ring → ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( 𝑁 ScMat 𝑅 ) ) ) )
55 3 54 biimtrdi ⊢ ( 𝑁 ∈ 𝑉 → ( ( ♯ ‘ 𝑁 ) = 1 → ( 𝑅 ∈ Ring → ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( 𝑁 ScMat 𝑅 ) ) ) ) )
56 55 3imp ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( ♯ ‘ 𝑁 ) = 1 ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( 𝑁 ScMat 𝑅 ) ) )