Theorem funcringcsetcALTV2lem9

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

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

Proof

Step	Hyp	Ref	Expression
1		funcringcsetcALTV2.r	⊢ 𝑅 = ( RingCat ‘ 𝑈 )
2		funcringcsetcALTV2.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
3		funcringcsetcALTV2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		funcringcsetcALTV2.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
5		funcringcsetcALTV2.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
6		funcringcsetcALTV2.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
7		funcringcsetcALTV2.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
8	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑈 ∈ WUni )
9		eqid	⊢ ( Hom ‘ 𝑅 ) = ( Hom ‘ 𝑅 )
10		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
11		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
12	1 3 8 9 10 11	ringchom	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )
13	12	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) ↔ 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ) )
14		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
15	1 3 8 9 11 14	ringchom	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ( 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	funcringcsetcALTV2lem5	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐺 𝑍 ) = ( 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	1 3 5	ringcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
29		inss1	⊢ ( 𝑈 ∩ Ring ) ⊆ 𝑈
30	28 29	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
31	30	sseld	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝑈 ) )
32	31	com12	⊢ ( 𝑋 ∈ 𝐵 → ( 𝜑 → 𝑋 ∈ 𝑈 ) )
33	32	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝜑 → 𝑋 ∈ 𝑈 ) )
34	33	impcom	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝑈 )
35	34	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝑋 ∈ 𝑈 )
36	30	sseld	⊢ ( 𝜑 → ( 𝑌 ∈ 𝐵 → 𝑌 ∈ 𝑈 ) )
37	36	com12	⊢ ( 𝑌 ∈ 𝐵 → ( 𝜑 → 𝑌 ∈ 𝑈 ) )
38	37	3ad2ant2	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝜑 → 𝑌 ∈ 𝑈 ) )
39	38	impcom	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝑈 )
40	39	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝑌 ∈ 𝑈 )
41	30	sseld	⊢ ( 𝜑 → ( 𝑍 ∈ 𝐵 → 𝑍 ∈ 𝑈 ) )
42	41	com12	⊢ ( 𝑍 ∈ 𝐵 → ( 𝜑 → 𝑍 ∈ 𝑈 ) )
43	42	3ad2ant3	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝜑 → 𝑍 ∈ 𝑈 ) )
44	43	impcom	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝑈 )
45	44	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝑍 ∈ 𝑈 )
46		eqid	⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
47		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
48	46 47	rhmf	⊢ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) → 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
49	48	ad2antrl	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
50		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
51	47 50	rhmf	⊢ ( 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) → 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) )
52	51	ad2antll	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) )
53	1 26 27 35 40 45 49 52	ringcco	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) = ( 𝐾 ∘ 𝐻 ) )
54	25 53	fveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( I ↾ ( 𝑋 RingHom 𝑍 ) ) ‘ ( 𝐾 ∘ 𝐻 ) ) )
55		eqid	⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
56	1 2 3 4 5 6	funcringcsetcALTV2lem2	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
57	56	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
58	57	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
59	1 2 3 4 5 6	funcringcsetcALTV2lem2	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
60	59	3ad2antr2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
61	60	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
62	1 2 3 4 5 6	funcringcsetcALTV2lem2	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
63	62	3ad2antr3	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
64	63	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
65	1 2 3 4 5 6	funcringcsetcALTV2lem1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) = ( Base ‘ 𝑋 ) )
66	65	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) = ( Base ‘ 𝑋 ) )
67	1 2 3 4 5 6	funcringcsetcALTV2lem1	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
68	67	3ad2antr2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
69	66 68	feq23d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ↔ 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) )
70	69	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ↔ 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) )
71	49 70	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) )
72		simpll	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝜑 )
73		3simpa	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
74	73	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
75		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) )
76	1 2 3 4 5 6 7	funcringcsetcALTV2lem6	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) = 𝐻 )
77	72 74 75 76	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) = 𝐻 )
78	77	feq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ↔ 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ) )
79	71 78	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) )
80	1 2 3 4 5 6	funcringcsetcALTV2lem1	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑍 ) = ( Base ‘ 𝑍 ) )
81	80	3ad2antr3	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑍 ) = ( Base ‘ 𝑍 ) )
82	68 81	feq23d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ↔ 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) ) )
83	82	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ↔ 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) ) )
84	52 83	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) )
85		3simpc	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) )
86	85	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) )
87		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) )
88	1 2 3 4 5 6 7	funcringcsetcALTV2lem6	⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) = 𝐾 )
89	72 86 87 88	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) = 𝐾 )
90	89	feq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ↔ 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ) )
91	84 90	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) )
92	2 26 55 58 61 64 79 91	setcco	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ∘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )
93	89 77	coeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ∘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
94	92 93	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
95	22 54 94	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )
96	95	ex	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝐻 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 RingHom 𝑍 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) )
97	17 96	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) )
98	97	3impia	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )