This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) )