Metamath Proof Explorer

Theorem ringcomlem

Description: Lemma for ringcom . This (formerly) part of the proof for ringcom is also applicable for semirings (without using the commutativity of the addition given per definition of a semiring), see srgcom4lem . (Contributed by GΓ©rard Lang, 4-Dec-2014) Variant of rglcom4d for rings. (Revised by AV, 5-Feb-2025)

Ref Expression
Hypotheses ringacl.b ⊒ 𝐡 = ( Base β€˜ 𝑅 )
ringacl.p ⊒ + = ( +g β€˜ 𝑅 )
Assertion ringcomlem ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ) β†’ ( ( 𝑋 + 𝑋 ) + ( π‘Œ + π‘Œ ) ) = ( ( 𝑋 + π‘Œ ) + ( 𝑋 + π‘Œ ) ) )

Proof

Step Hyp Ref Expression
1 ringacl.b ⊒ 𝐡 = ( Base β€˜ 𝑅 )
2 ringacl.p ⊒ + = ( +g β€˜ 𝑅 )
3 eqid ⊒ ( .r β€˜ 𝑅 ) = ( .r β€˜ 𝑅 )
4 1 2 3 ringdir ⊒ ( ( 𝑅 ∈ Ring ∧ ( π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡 ) ) β†’ ( ( π‘₯ + 𝑦 ) ( .r β€˜ 𝑅 ) 𝑧 ) = ( ( π‘₯ ( .r β€˜ 𝑅 ) 𝑧 ) + ( 𝑦 ( .r β€˜ 𝑅 ) 𝑧 ) ) )
5 4 ralrimivvva ⊒ ( 𝑅 ∈ Ring β†’ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 βˆ€ 𝑧 ∈ 𝐡 ( ( π‘₯ + 𝑦 ) ( .r β€˜ 𝑅 ) 𝑧 ) = ( ( π‘₯ ( .r β€˜ 𝑅 ) 𝑧 ) + ( 𝑦 ( .r β€˜ 𝑅 ) 𝑧 ) ) )
6 5 3ad2ant1 ⊒ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ) β†’ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 βˆ€ 𝑧 ∈ 𝐡 ( ( π‘₯ + 𝑦 ) ( .r β€˜ 𝑅 ) 𝑧 ) = ( ( π‘₯ ( .r β€˜ 𝑅 ) 𝑧 ) + ( 𝑦 ( .r β€˜ 𝑅 ) 𝑧 ) ) )
7 eqid ⊒ ( 1r β€˜ 𝑅 ) = ( 1r β€˜ 𝑅 )
8 1 7 ringidcl ⊒ ( 𝑅 ∈ Ring β†’ ( 1r β€˜ 𝑅 ) ∈ 𝐡 )
9 8 3ad2ant1 ⊒ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ) β†’ ( 1r β€˜ 𝑅 ) ∈ 𝐡 )
10 1 3 7 ringlidm ⊒ ( ( 𝑅 ∈ Ring ∧ π‘₯ ∈ 𝐡 ) β†’ ( ( 1r β€˜ 𝑅 ) ( .r β€˜ 𝑅 ) π‘₯ ) = π‘₯ )
11 10 ralrimiva ⊒ ( 𝑅 ∈ Ring β†’ βˆ€ π‘₯ ∈ 𝐡 ( ( 1r β€˜ 𝑅 ) ( .r β€˜ 𝑅 ) π‘₯ ) = π‘₯ )
12 11 3ad2ant1 ⊒ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ) β†’ βˆ€ π‘₯ ∈ 𝐡 ( ( 1r β€˜ 𝑅 ) ( .r β€˜ 𝑅 ) π‘₯ ) = π‘₯ )
13 simp2 ⊒ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ) β†’ 𝑋 ∈ 𝐡 )
14 1 2 ringacl ⊒ ( ( 𝑅 ∈ Ring ∧ π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ) β†’ ( π‘₯ + 𝑦 ) ∈ 𝐡 )
15 14 3expb ⊒ ( ( 𝑅 ∈ Ring ∧ ( π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ) ) β†’ ( π‘₯ + 𝑦 ) ∈ 𝐡 )
16 15 ralrimivva ⊒ ( 𝑅 ∈ Ring β†’ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( π‘₯ + 𝑦 ) ∈ 𝐡 )
17 16 3ad2ant1 ⊒ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ) β†’ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( π‘₯ + 𝑦 ) ∈ 𝐡 )
18 1 2 3 ringdi ⊒ ( ( 𝑅 ∈ Ring ∧ ( π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡 ) ) β†’ ( π‘₯ ( .r β€˜ 𝑅 ) ( 𝑦 + 𝑧 ) ) = ( ( π‘₯ ( .r β€˜ 𝑅 ) 𝑦 ) + ( π‘₯ ( .r β€˜ 𝑅 ) 𝑧 ) ) )
19 18 ralrimivvva ⊒ ( 𝑅 ∈ Ring β†’ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ ( .r β€˜ 𝑅 ) ( 𝑦 + 𝑧 ) ) = ( ( π‘₯ ( .r β€˜ 𝑅 ) 𝑦 ) + ( π‘₯ ( .r β€˜ 𝑅 ) 𝑧 ) ) )
20 19 3ad2ant1 ⊒ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ) β†’ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ ( .r β€˜ 𝑅 ) ( 𝑦 + 𝑧 ) ) = ( ( π‘₯ ( .r β€˜ 𝑅 ) 𝑦 ) + ( π‘₯ ( .r β€˜ 𝑅 ) 𝑧 ) ) )
21 simp3 ⊒ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ) β†’ π‘Œ ∈ 𝐡 )
22 6 9 12 13 17 20 21 rglcom4d ⊒ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ) β†’ ( ( 𝑋 + 𝑋 ) + ( π‘Œ + π‘Œ ) ) = ( ( 𝑋 + π‘Œ ) + ( 𝑋 + π‘Œ ) ) )