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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )