Theorem opprmulfval

Description: Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	opprval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	opprval.2	⊢ · = ( .r ‘ 𝑅 )
	opprval.3	⊢ 𝑂 = ( oppr ‘ 𝑅 )
	opprmulfval.4	⊢ ∙ = ( .r ‘ 𝑂 )
Assertion	opprmulfval	⊢ ∙ = tpos ·

Proof

Step	Hyp	Ref	Expression
1		opprval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		opprval.2	⊢ · = ( .r ‘ 𝑅 )
3		opprval.3	⊢ 𝑂 = ( oppr ‘ 𝑅 )
4		opprmulfval.4	⊢ ∙ = ( .r ‘ 𝑂 )
5	1 2 3	opprval	⊢ 𝑂 = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ )
6	5	fveq2i	⊢ ( .r ‘ 𝑂 ) = ( .r ‘ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) )
7	2	fvexi	⊢ · ∈ V
8	7	tposex	⊢ tpos · ∈ V
9		mulrid	⊢ .r = Slot ( .r ‘ ndx )
10	9	setsid	⊢ ( ( 𝑅 ∈ V ∧ tpos · ∈ V ) → tpos · = ( .r ‘ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) ) )
11	8 10	mpan2	⊢ ( 𝑅 ∈ V → tpos · = ( .r ‘ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) ) )
12	6 11	eqtr4id	⊢ ( 𝑅 ∈ V → ( .r ‘ 𝑂 ) = tpos · )
13		tpos0	⊢ tpos ∅ = ∅
14	9	str0	⊢ ∅ = ( .r ‘ ∅ )
15	13 14	eqtr2i	⊢ ( .r ‘ ∅ ) = tpos ∅
16		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( oppr ‘ 𝑅 ) = ∅ )
17	3 16	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝑂 = ∅ )
18	17	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( .r ‘ 𝑂 ) = ( .r ‘ ∅ ) )
19		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( .r ‘ 𝑅 ) = ∅ )
20	2 19	syl5eq	⊢ ( ¬ 𝑅 ∈ V → · = ∅ )
21	20	tposeqd	⊢ ( ¬ 𝑅 ∈ V → tpos · = tpos ∅ )
22	15 18 21	3eqtr4a	⊢ ( ¬ 𝑅 ∈ V → ( .r ‘ 𝑂 ) = tpos · )
23	12 22	pm2.61i	⊢ ( .r ‘ 𝑂 ) = tpos ·
24	4 23	eqtri	⊢ ∙ = tpos ·