Metamath Proof Explorer

Theorem mat1dimcrng

Description: The algebra of matrices with dimension 1 over a commutative ring is a commutative ring. (Contributed by AV, 16-Aug-2019)

Ref Expression
Hypotheses mat1dim.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
Assertion mat1dimcrng ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → 𝐴 ∈ CRing )

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
2 mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
4 snfi ⊢ { 𝐸 } ∈ Fin
5 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6 5 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Ring )
7 1 matring ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
8 4 6 7 sylancr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → 𝐴 ∈ Ring )
9 1 2 3 mat1dimelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑎 ∈ 𝐵 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ) )
10 1 2 3 mat1dimelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑦 ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } ) )
11 9 10 anbi12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ↔ ( ∃ 𝑎 ∈ 𝐵 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ∧ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } ) ) )
12 5 11 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ↔ ( ∃ 𝑎 ∈ 𝐵 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ∧ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } ) ) )
13 simpll ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑅 ∈ CRing )
14 simprl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
15 simprr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
16 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
17 2 16 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) )
18 13 14 15 17 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) )
19 18 opeq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ⟨ 𝑂 , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ⟩ = ⟨ 𝑂 , ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ⟩ )
20 19 sneqd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → { ⟨ 𝑂 , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ⟩ } = { ⟨ 𝑂 , ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ⟩ } )
21 5 anim1i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) )
22 1 2 3 mat1dimmul ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑎 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑏 ⟩ } ) = { ⟨ 𝑂 , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ⟩ } )
23 21 22 sylan ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑎 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑏 ⟩ } ) = { ⟨ 𝑂 , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ⟩ } )
24 pm3.22 ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) )
25 1 2 3 mat1dimmul ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) = { ⟨ 𝑂 , ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ⟩ } )
26 21 24 25 syl2an ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) = { ⟨ 𝑂 , ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ⟩ } )
27 20 23 26 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( { ⟨ 𝑂 , 𝑎 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑏 ⟩ } ) = ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) )
28 27 expr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐵 → ( { ⟨ 𝑂 , 𝑎 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑏 ⟩ } ) = ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) ) )
29 28 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ) → ( 𝑏 ∈ 𝐵 → ( { ⟨ 𝑂 , 𝑎 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑏 ⟩ } ) = ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) ) )
30 29 imp ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ) ∧ 𝑏 ∈ 𝐵 ) → ( { ⟨ 𝑂 , 𝑎 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑏 ⟩ } ) = ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) )
31 30 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } ) → ( { ⟨ 𝑂 , 𝑎 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑏 ⟩ } ) = ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) )
32 oveq12 ⊢ ( ( 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ∧ 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( { ⟨ 𝑂 , 𝑎 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑏 ⟩ } ) )
33 32 ad4ant24 ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( { ⟨ 𝑂 , 𝑎 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑏 ⟩ } ) )
34 oveq12 ⊢ ( ( 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } ∧ 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ) → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) )
35 34 expcom ⊢ ( 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } → ( 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) ) )
36 35 ad2antlr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) ) )
37 36 imp ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } ) → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( { ⟨ 𝑂 , 𝑏 ⟩ } ( .r ‘ 𝐴 ) { ⟨ 𝑂 , 𝑎 ⟩ } ) )
38 31 33 37 3eqtr4d ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) )
39 38 rexlimdva2 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ) → ( ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
40 39 rexlimdva2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ( ∃ 𝑎 ∈ 𝐵 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } → ( ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) ) )
41 40 impd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ( ( ∃ 𝑎 ∈ 𝐵 𝑥 = { ⟨ 𝑂 , 𝑎 ⟩ } ∧ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑂 , 𝑏 ⟩ } ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
42 12 41 sylbid ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
43 42 ralrimivv ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) )
44 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
45 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
46 44 45 iscrng2 ⊢ ( 𝐴 ∈ CRing ↔ ( 𝐴 ∈ Ring ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
47 8 43 46 sylanbrc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉 ) → 𝐴 ∈ CRing )