Metamath Proof Explorer

Theorem srngadd

Description: The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses srngcl.i ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
srngcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
srngadd.p ⊢ + = ( +g ‘ 𝑅 )
Assertion srngadd ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∗ ‘ ( 𝑋 + 𝑌 ) ) = ( ( ∗ ‘ 𝑋 ) + ( ∗ ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 srngcl.i ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
2 srngcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 srngadd.p ⊢ + = ( +g ‘ 𝑅 )
4 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
5 eqid ⊢ ( *rf ‘ 𝑅 ) = ( *rf ‘ 𝑅 )
6 4 5 srngrhm ⊢ ( 𝑅 ∈ *-Ring → ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) )
7 rhmghm ⊢ ( ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) → ( *rf ‘ 𝑅 ) ∈ ( 𝑅 GrpHom ( oppr ‘ 𝑅 ) ) )
8 6 7 syl ⊢ ( 𝑅 ∈ *-Ring → ( *rf ‘ 𝑅 ) ∈ ( 𝑅 GrpHom ( oppr ‘ 𝑅 ) ) )
9 4 3 oppradd ⊢ + = ( +g ‘ ( oppr ‘ 𝑅 ) )
10 2 3 9 ghmlin ⊢ ( ( ( *rf ‘ 𝑅 ) ∈ ( 𝑅 GrpHom ( oppr ‘ 𝑅 ) ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ ( 𝑋 + 𝑌 ) ) = ( ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) + ( ( *rf ‘ 𝑅 ) ‘ 𝑌 ) ) )
11 8 10 syl3an1 ⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ ( 𝑋 + 𝑌 ) ) = ( ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) + ( ( *rf ‘ 𝑅 ) ‘ 𝑌 ) ) )
12 srngring ⊢ ( 𝑅 ∈ *-Ring → 𝑅 ∈ Ring )
13 2 3 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
14 12 13 syl3an1 ⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
15 2 1 5 stafval ⊢ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 → ( ( *rf ‘ 𝑅 ) ‘ ( 𝑋 + 𝑌 ) ) = ( ∗ ‘ ( 𝑋 + 𝑌 ) ) )
16 14 15 syl ⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ ( 𝑋 + 𝑌 ) ) = ( ∗ ‘ ( 𝑋 + 𝑌 ) ) )
17 2 1 5 stafval ⊢ ( 𝑋 ∈ 𝐵 → ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) = ( ∗ ‘ 𝑋 ) )
18 17 3ad2ant2 ⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) = ( ∗ ‘ 𝑋 ) )
19 2 1 5 stafval ⊢ ( 𝑌 ∈ 𝐵 → ( ( *rf ‘ 𝑅 ) ‘ 𝑌 ) = ( ∗ ‘ 𝑌 ) )
20 19 3ad2ant3 ⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ 𝑌 ) = ( ∗ ‘ 𝑌 ) )
21 18 20 oveq12d ⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) + ( ( *rf ‘ 𝑅 ) ‘ 𝑌 ) ) = ( ( ∗ ‘ 𝑋 ) + ( ∗ ‘ 𝑌 ) ) )
22 11 16 21 3eqtr3d ⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∗ ‘ ( 𝑋 + 𝑌 ) ) = ( ( ∗ ‘ 𝑋 ) + ( ∗ ‘ 𝑌 ) ) )