Theorem funcringcsetclem9ALTV

Description: Lemma 9 for funcringcsetcALTV . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	funcringcsetcALTV.r	⊢ 𝑅 = ( RingCatALTV ‘ 𝑈 )
	funcringcsetcALTV.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	funcringcsetcALTV.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	funcringcsetcALTV.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
	funcringcsetcALTV.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	funcringcsetcALTV.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
	funcringcsetcALTV.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
Assertion	funcringcsetclem9ALTV	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funcringcsetcALTV.r	⊢ 𝑅 = ( RingCatALTV ‘ 𝑈 )
2		funcringcsetcALTV.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
3		funcringcsetcALTV.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		funcringcsetcALTV.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
5		funcringcsetcALTV.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
6		funcringcsetcALTV.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
7		funcringcsetcALTV.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
8	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑈 ∈ WUni )
9		eqid	⊢ ( Hom ‘ 𝑅 ) = ( Hom ‘ 𝑅 )
10		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
11		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
12	1 3 8 9 10 11	ringchomALTV	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )
13	12	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) ↔ 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ) )
14		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
15	1 3 8 9 11 14	ringchomALTV	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) = ( 𝑌 RingHom 𝑍 ) )
16	15	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) ↔ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) )
17	13 16	anbi12d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) ) ↔ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) )
18		rhmco	⊢ ( ( 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ∧ 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ) → ( 𝐾 ∘ 𝐻 ) ∈ ( 𝑋 RingHom 𝑍 ) )
19	18	ancoms	⊢ ( ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) → ( 𝐾 ∘ 𝐻 ) ∈ ( 𝑋 RingHom 𝑍 ) )
20	19	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐾 ∘ 𝐻 ) ∈ ( 𝑋 RingHom 𝑍 ) )
21		fvresi	⊢ ( ( 𝐾 ∘ 𝐻 ) ∈ ( 𝑋 RingHom 𝑍 ) → ( ( I ↾ ( 𝑋 RingHom 𝑍 ) ) ‘ ( 𝐾 ∘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
22	20 21	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( I ↾ ( 𝑋 RingHom 𝑍 ) ) ‘ ( 𝐾 ∘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
23	1 2 3 4 5 6 7	funcringcsetclem5ALTV	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐺 𝑍 ) = ( I ↾ ( 𝑋 RingHom 𝑍 ) ) )
24	23	3adantr2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐺 𝑍 ) = ( I ↾ ( 𝑋 RingHom 𝑍 ) ) )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝑋 𝐺 𝑍 ) = ( I ↾ ( 𝑋 RingHom 𝑍 ) ) )
26	8	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝑈 ∈ WUni )
27		eqid	⊢ ( comp ‘ 𝑅 ) = ( comp ‘ 𝑅 )
28	10	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝑋 ∈ 𝐵 )
29	11	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝑌 ∈ 𝐵 )
30	14	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝑍 ∈ 𝐵 )
31		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) )
32		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) )
33	1 3 26 27 28 29 30 31 32	ringccoALTV	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) = ( 𝐾 ∘ 𝐻 ) )
34	25 33	fveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( I ↾ ( 𝑋 RingHom 𝑍 ) ) ‘ ( 𝐾 ∘ 𝐻 ) ) )
35		eqid	⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
36	1 2 3 4 5 6	funcringcsetclem2ALTV	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
37	36	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
38	37	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
39	1 2 3 4 5 6	funcringcsetclem2ALTV	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
40	39	3ad2antr2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
41	40	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
42	1 2 3 4 5 6	funcringcsetclem2ALTV	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
43	42	3ad2antr3	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
44	43	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
45		eqid	⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
46		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
47	45 46	rhmf	⊢ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) → 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
48	47	ad2antrl	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
49	1 2 3 4 5 6	funcringcsetclem1ALTV	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) = ( Base ‘ 𝑋 ) )
50	49	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) = ( Base ‘ 𝑋 ) )
51	1 2 3 4 5 6	funcringcsetclem1ALTV	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
52	51	3ad2antr2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
53	50 52	feq23d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ↔ 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) )
54	53	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ↔ 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) )
55	48 54	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) )
56		simpll	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝜑 )
57		3simpa	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
58	57	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
59	1 2 3 4 5 6 7	funcringcsetclem6ALTV	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) = 𝐻 )
60	56 58 31 59	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) = 𝐻 )
61	60	feq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ↔ 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ) )
62	55 61	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) )
63		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
64	46 63	rhmf	⊢ ( 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) → 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) )
65	64	ad2antll	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) )
66	1 2 3 4 5 6	funcringcsetclem1ALTV	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑍 ) = ( Base ‘ 𝑍 ) )
67	66	3ad2antr3	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑍 ) = ( Base ‘ 𝑍 ) )
68	52 67	feq23d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ↔ 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) ) )
69	68	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ↔ 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) ) )
70	65 69	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) )
71		3simpc	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) )
72	71	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) )
73	1 2 3 4 5 6 7	funcringcsetclem6ALTV	⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) = 𝐾 )
74	56 72 32 73	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) = 𝐾 )
75	74	feq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ↔ 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ) )
76	70 75	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) )
77	2 26 35 38 41 44 62 76	setcco	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ∘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )
78	74 60	coeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ∘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
79	77 78	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
80	22 34 79	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )
81	80	ex	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) )
82	17 81	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) )
83	82	3impia	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )