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 )