Theorem isthincd2lem2

Description: Lemma for isthincd2 . (Contributed by Zhi Wang, 17-Sep-2024)

	Ref	Expression
Hypotheses	isthincd2lem2.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	isthincd2lem2.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	isthincd2lem2.3	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	isthincd2lem2.4	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	isthincd2lem2.5	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
	isthincd2lem2.6	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
Assertion	isthincd2lem2	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		isthincd2lem2.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
2		isthincd2lem2.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
3		isthincd2lem2.3	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
4		isthincd2lem2.4	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
5		isthincd2lem2.5	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
6		isthincd2lem2.6	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
7		oveq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝐻 𝑦 ) = ( 𝑤 𝐻 𝑦 ) )
8		opeq1	⊢ ( 𝑥 = 𝑤 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑤 , 𝑦 ⟩ )
9	8	oveq1d	⊢ ( 𝑥 = 𝑤 → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑤 , 𝑦 ⟩ · 𝑧 ) )
10	9	oveqd	⊢ ( 𝑥 = 𝑤 → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑤 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) )
11		oveq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝐻 𝑧 ) = ( 𝑤 𝐻 𝑧 ) )
12	10 11	eleq12d	⊢ ( 𝑥 = 𝑤 → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ↔ ( 𝑔 ( ⟨ 𝑤 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ) )
13	12	ralbidv	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ↔ ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ) )
14	7 13	raleqbidv	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ↔ ∀ 𝑓 ∈ ( 𝑤 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ) )
15		oveq2	⊢ ( 𝑦 = 𝑣 → ( 𝑤 𝐻 𝑦 ) = ( 𝑤 𝐻 𝑣 ) )
16		oveq1	⊢ ( 𝑦 = 𝑣 → ( 𝑦 𝐻 𝑧 ) = ( 𝑣 𝐻 𝑧 ) )
17		opeq2	⊢ ( 𝑦 = 𝑣 → ⟨ 𝑤 , 𝑦 ⟩ = ⟨ 𝑤 , 𝑣 ⟩ )
18	17	oveq1d	⊢ ( 𝑦 = 𝑣 → ( ⟨ 𝑤 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) )
19	18	oveqd	⊢ ( 𝑦 = 𝑣 → ( 𝑔 ( ⟨ 𝑤 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) 𝑓 ) )
20	19	eleq1d	⊢ ( 𝑦 = 𝑣 → ( ( 𝑔 ( ⟨ 𝑤 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ↔ ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ) )
21	16 20	raleqbidv	⊢ ( 𝑦 = 𝑣 → ( ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ↔ ∀ 𝑔 ∈ ( 𝑣 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ) )
22	15 21	raleqbidv	⊢ ( 𝑦 = 𝑣 → ( ∀ 𝑓 ∈ ( 𝑤 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ↔ ∀ 𝑓 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑔 ∈ ( 𝑣 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ) )
23		oveq2	⊢ ( 𝑧 = 𝑢 → ( 𝑣 𝐻 𝑧 ) = ( 𝑣 𝐻 𝑢 ) )
24		oveq2	⊢ ( 𝑧 = 𝑢 → ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) = ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) )
25	24	oveqd	⊢ ( 𝑧 = 𝑢 → ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑓 ) )
26		oveq2	⊢ ( 𝑧 = 𝑢 → ( 𝑤 𝐻 𝑧 ) = ( 𝑤 𝐻 𝑢 ) )
27	25 26	eleq12d	⊢ ( 𝑧 = 𝑢 → ( ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ↔ ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑢 ) ) )
28	23 27	raleqbidv	⊢ ( 𝑧 = 𝑢 → ( ∀ 𝑔 ∈ ( 𝑣 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ↔ ∀ 𝑔 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑢 ) ) )
29	28	ralbidv	⊢ ( 𝑧 = 𝑢 → ( ∀ 𝑓 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑔 ∈ ( 𝑣 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ↔ ∀ 𝑓 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑔 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑢 ) ) )
30		oveq2	⊢ ( 𝑓 = 𝑘 → ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) )
31	30	eleq1d	⊢ ( 𝑓 = 𝑘 → ( ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑢 ) ↔ ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) ) )
32		oveq1	⊢ ( 𝑔 = 𝑙 → ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) = ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) )
33	32	eleq1d	⊢ ( 𝑔 = 𝑙 → ( ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) ↔ ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) ) )
34	31 33	cbvral2vw	⊢ ( ∀ 𝑓 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑔 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑢 ) ↔ ∀ 𝑘 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) )
35	29 34	bitrdi	⊢ ( 𝑧 = 𝑢 → ( ∀ 𝑓 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑔 ∈ ( 𝑣 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑤 𝐻 𝑧 ) ↔ ∀ 𝑘 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) ) )
36	14 22 35	cbvral3vw	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) )
37	6 36	sylib	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) )
38		oveq1	⊢ ( 𝑤 = 𝑋 → ( 𝑤 𝐻 𝑣 ) = ( 𝑋 𝐻 𝑣 ) )
39		opeq1	⊢ ( 𝑤 = 𝑋 → ⟨ 𝑤 , 𝑣 ⟩ = ⟨ 𝑋 , 𝑣 ⟩ )
40	39	oveq1d	⊢ ( 𝑤 = 𝑋 → ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) = ( ⟨ 𝑋 , 𝑣 ⟩ · 𝑢 ) )
41	40	oveqd	⊢ ( 𝑤 = 𝑋 → ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) = ( 𝑙 ( ⟨ 𝑋 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) )
42		oveq1	⊢ ( 𝑤 = 𝑋 → ( 𝑤 𝐻 𝑢 ) = ( 𝑋 𝐻 𝑢 ) )
43	41 42	eleq12d	⊢ ( 𝑤 = 𝑋 → ( ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) ↔ ( 𝑙 ( ⟨ 𝑋 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ) )
44	43	ralbidv	⊢ ( 𝑤 = 𝑋 → ( ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) ↔ ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑋 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ) )
45	38 44	raleqbidv	⊢ ( 𝑤 = 𝑋 → ( ∀ 𝑘 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) ↔ ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑣 ) ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑋 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ) )
46		oveq2	⊢ ( 𝑣 = 𝑌 → ( 𝑋 𝐻 𝑣 ) = ( 𝑋 𝐻 𝑌 ) )
47		oveq1	⊢ ( 𝑣 = 𝑌 → ( 𝑣 𝐻 𝑢 ) = ( 𝑌 𝐻 𝑢 ) )
48		opeq2	⊢ ( 𝑣 = 𝑌 → ⟨ 𝑋 , 𝑣 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
49	48	oveq1d	⊢ ( 𝑣 = 𝑌 → ( ⟨ 𝑋 , 𝑣 ⟩ · 𝑢 ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑢 ) )
50	49	oveqd	⊢ ( 𝑣 = 𝑌 → ( 𝑙 ( ⟨ 𝑋 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑢 ) 𝑘 ) )
51	50	eleq1d	⊢ ( 𝑣 = 𝑌 → ( ( 𝑙 ( ⟨ 𝑋 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ↔ ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ) )
52	47 51	raleqbidv	⊢ ( 𝑣 = 𝑌 → ( ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑋 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ↔ ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ) )
53	46 52	raleqbidv	⊢ ( 𝑣 = 𝑌 → ( ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑣 ) ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑋 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ↔ ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ) )
54		oveq2	⊢ ( 𝑢 = 𝑍 → ( 𝑌 𝐻 𝑢 ) = ( 𝑌 𝐻 𝑍 ) )
55		oveq2	⊢ ( 𝑢 = 𝑍 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑢 ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) )
56	55	oveqd	⊢ ( 𝑢 = 𝑍 → ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑢 ) 𝑘 ) = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) )
57		oveq2	⊢ ( 𝑢 = 𝑍 → ( 𝑋 𝐻 𝑢 ) = ( 𝑋 𝐻 𝑍 ) )
58	56 57	eleq12d	⊢ ( 𝑢 = 𝑍 → ( ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ↔ ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
59	54 58	raleqbidv	⊢ ( 𝑢 = 𝑍 → ( ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ↔ ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑍 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
60	59	ralbidv	⊢ ( 𝑢 = 𝑍 → ( ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑢 ) ↔ ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑍 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
61	45 53 60	rspc3v	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) → ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑍 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
62	1 2 3 61	syl3anc	⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑤 𝐻 𝑣 ) ∀ 𝑙 ∈ ( 𝑣 𝐻 𝑢 ) ( 𝑙 ( ⟨ 𝑤 , 𝑣 ⟩ · 𝑢 ) 𝑘 ) ∈ ( 𝑤 𝐻 𝑢 ) → ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑍 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
63	37 62	mpd	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑍 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑍 ) )
64		oveq2	⊢ ( 𝑘 = 𝐹 → ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
65	64	eleq1d	⊢ ( 𝑘 = 𝐹 → ( ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑍 ) ↔ ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
66		oveq1	⊢ ( 𝑙 = 𝐺 → ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
67	66	eleq1d	⊢ ( 𝑙 = 𝐺 → ( ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ↔ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
68	65 67	rspc2v	⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑍 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑍 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
69	4 5 68	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑌 𝐻 𝑍 ) ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑘 ) ∈ ( 𝑋 𝐻 𝑍 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
70	63 69	mpd	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) )