Theorem ringccoALTV

Description: Composition in the category of rings. (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ringcbasALTV.c	⊢ 𝐶 = ( RingCatALTV ‘ 𝑈 )
	ringcbasALTV.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	ringcbasALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	ringccoALTV.o	⊢ · = ( comp ‘ 𝐶 )
	ringccoALTV.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	ringccoALTV.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	ringccoALTV.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	ringccoALTV.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) )
	ringccoALTV.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 RingHom 𝑍 ) )
Assertion	ringccoALTV	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ringcbasALTV.c	⊢ 𝐶 = ( RingCatALTV ‘ 𝑈 )
2		ringcbasALTV.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		ringcbasALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4		ringccoALTV.o	⊢ · = ( comp ‘ 𝐶 )
5		ringccoALTV.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		ringccoALTV.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		ringccoALTV.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		ringccoALTV.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) )
9		ringccoALTV.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 RingHom 𝑍 ) )
10	1 2 3 4	ringccofvalALTV	⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
11		simprl	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑣 ) = ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
13		op2ndg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
14	5 6 13	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
16	12 15	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑣 ) = 𝑌 )
17		simprr	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑧 = 𝑍 )
18	16 17	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) = ( 𝑌 RingHom 𝑍 ) )
19	11	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ 𝑣 ) = ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
20		op1stg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
21	5 6 20	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
22	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
23	19 22	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ 𝑣 ) = 𝑋 )
24	23 16	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) = ( 𝑋 RingHom 𝑌 ) )
25		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∘ 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
26	18 24 25	mpoeq123dv	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ ( 𝑌 RingHom 𝑍 ) , 𝑓 ∈ ( 𝑋 RingHom 𝑌 ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
27		opelxpi	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
28	5 6 27	syl2anc	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
29		ovex	⊢ ( 𝑌 RingHom 𝑍 ) ∈ V
30		ovex	⊢ ( 𝑋 RingHom 𝑌 ) ∈ V
31	29 30	mpoex	⊢ ( 𝑔 ∈ ( 𝑌 RingHom 𝑍 ) , 𝑓 ∈ ( 𝑋 RingHom 𝑌 ) ↦ ( 𝑔 ∘ 𝑓 ) ) ∈ V
32	31	a1i	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑌 RingHom 𝑍 ) , 𝑓 ∈ ( 𝑋 RingHom 𝑌 ) ↦ ( 𝑔 ∘ 𝑓 ) ) ∈ V )
33	10 26 28 7 32	ovmpod	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) = ( 𝑔 ∈ ( 𝑌 RingHom 𝑍 ) , 𝑓 ∈ ( 𝑋 RingHom 𝑌 ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
34		simprl	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑔 = 𝐺 )
35		simprr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
36	34 35	coeq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝑔 ∘ 𝑓 ) = ( 𝐺 ∘ 𝐹 ) )
37		coexg	⊢ ( ( 𝐺 ∈ ( 𝑌 RingHom 𝑍 ) ∧ 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ) → ( 𝐺 ∘ 𝐹 ) ∈ V )
38	9 8 37	syl2anc	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ V )
39	33 36 9 8 38	ovmpod	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )