Theorem m2detleiblem7

Description: Lemma 7 for m2detleib . (Contributed by AV, 20-Dec-2018)

	Ref	Expression
Hypotheses	m2detleiblem1.n	⊢ 𝑁 = { 1 , 2 }
	m2detleiblem1.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	m2detleiblem1.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
	m2detleiblem1.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
	m2detleiblem1.o	⊢ 1 = ( 1r ‘ 𝑅 )
	m2detleiblem1.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
	m2detleiblem1.t	⊢ · = ( .r ‘ 𝑅 )
	m2detleiblem1.m	⊢ − = ( -g ‘ 𝑅 )
Assertion	m2detleiblem7	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑍 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑋 ( +g ‘ 𝑅 ) ( ( 𝐼 ‘ 1 ) · 𝑍 ) ) = ( 𝑋 − 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		m2detleiblem1.n	⊢ 𝑁 = { 1 , 2 }
2		m2detleiblem1.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
3		m2detleiblem1.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
4		m2detleiblem1.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
5		m2detleiblem1.o	⊢ 1 = ( 1r ‘ 𝑅 )
6		m2detleiblem1.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
7		m2detleiblem1.t	⊢ · = ( .r ‘ 𝑅 )
8		m2detleiblem1.m	⊢ − = ( -g ‘ 𝑅 )
9		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
11		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ ( Base ‘ 𝑅 ) ) → 𝑍 ∈ ( Base ‘ 𝑅 ) )
12	9 7 5 6 10 11	ringnegl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 ‘ 1 ) · 𝑍 ) = ( 𝐼 ‘ 𝑍 ) )
13	12	3adant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑍 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 ‘ 1 ) · 𝑍 ) = ( 𝐼 ‘ 𝑍 ) )
14	13	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑍 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑋 ( +g ‘ 𝑅 ) ( ( 𝐼 ‘ 1 ) · 𝑍 ) ) = ( 𝑋 ( +g ‘ 𝑅 ) ( 𝐼 ‘ 𝑍 ) ) )
15		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
16	9 15 6 8	grpsubval	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑍 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑋 − 𝑍 ) = ( 𝑋 ( +g ‘ 𝑅 ) ( 𝐼 ‘ 𝑍 ) ) )
17	16	3adant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑍 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑋 − 𝑍 ) = ( 𝑋 ( +g ‘ 𝑅 ) ( 𝐼 ‘ 𝑍 ) ) )
18	14 17	eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑍 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑋 ( +g ‘ 𝑅 ) ( ( 𝐼 ‘ 1 ) · 𝑍 ) ) = ( 𝑋 − 𝑍 ) )