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

Metamath Proof Explorer

Theorem iscatd2

Description: Version of iscatd with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses iscatd2.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
iscatd2.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
iscatd2.o ⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
iscatd2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
iscatd2.ps ⊢ ( 𝜓 ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
iscatd2.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 1 ∈ ( 𝑦 𝐻 𝑦 ) )
iscatd2.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 )
iscatd2.3 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 )
iscatd2.4 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
iscatd2.5 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
Assertion iscatd2 ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 1 ) ) )

Proof

Step Hyp Ref Expression
1 iscatd2.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2 iscatd2.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
3 iscatd2.o ⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
4 iscatd2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5 iscatd2.ps ⊢ ( 𝜓 ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
6 iscatd2.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 1 ∈ ( 𝑦 𝐻 𝑦 ) )
7 iscatd2.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 )
8 iscatd2.3 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 )
9 iscatd2.4 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
10 iscatd2.5 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
11 6 ne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 𝐻 𝑦 ) ≠ ∅ )
12 11 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) → ( 𝑦 𝐻 𝑦 ) ≠ ∅ )
13 n0 ⊢ ( ( 𝑦 𝐻 𝑦 ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) )
14 12 13 sylib ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) → ∃ 𝑔 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) )
15 n0 ⊢ ( ( 𝑦 𝐻 𝑦 ) ≠ ∅ ↔ ∃ 𝑘 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) )
16 12 15 sylib ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) → ∃ 𝑘 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) )
17 exdistrv ⊢ ( ∃ 𝑔 ∃ 𝑘 ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ↔ ( ∃ 𝑔 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ ∃ 𝑘 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) )
18 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) ∧ ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) → 𝜑 )
19 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) ∧ ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) → 𝑎 ∈ 𝐵 )
20 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) ∧ ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) → 𝑦 ∈ 𝐵 )
21 19 20 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) ∧ ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) → ( 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
22 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) ∧ ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) → 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) )
23 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) ∧ ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) → 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) )
24 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) ∧ ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) → 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) )
25 22 23 24 3jca ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) ∧ ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) → ( 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) )
26 simplll ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → 𝑥 = 𝑎 )
27 26 eleq1d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 𝑥 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵 ) )
28 27 anbi1d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
29 simpllr ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → 𝑧 = 𝑦 )
30 29 eleq1d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 𝑧 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
31 simplr ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → 𝑤 = 𝑦 )
32 31 eleq1d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 𝑤 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
33 30 32 anbi12d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
34 anidm ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ 𝑦 ∈ 𝐵 )
35 33 34 bitrdi ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ↔ 𝑦 ∈ 𝐵 ) )
36 simpr ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → 𝑓 = 𝑟 )
37 26 oveq1d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑎 𝐻 𝑦 ) )
38 36 37 eleq12d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) )
39 29 oveq2d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑦 𝐻 𝑦 ) )
40 39 eleq2d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ↔ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ) )
41 29 31 oveq12d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 𝑧 𝐻 𝑤 ) = ( 𝑦 𝐻 𝑦 ) )
42 41 eleq2d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ↔ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) )
43 38 40 42 3anbi123d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) )
44 28 35 43 3anbi123d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) ) )
45 5 44 bitrid ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 𝜓 ↔ ( ( 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) ) )
46 45 anbi2d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( ( 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) ) ) )
47 26 opeq1d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑦 ⟩ )
48 47 oveq1d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) = ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) )
49 eqidd ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → 1 = 1 )
50 48 49 36 oveq123d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) )
51 50 36 eqeq12d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 ↔ ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 ) )
52 46 51 imbi12d ⊢ ( ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) ∧ 𝑓 = 𝑟 ) → ( ( ( 𝜑 ∧ 𝜓 ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 ) ↔ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) ) → ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 ) ) )
53 52 sbiedvw ⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) ∧ 𝑤 = 𝑦 ) → ( [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 ) ↔ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) ) → ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 ) ) )
54 53 sbiedvw ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑧 = 𝑦 ) → ( [ 𝑦 / 𝑤 ] [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 ) ↔ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) ) → ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 ) ) )
55 54 sbiedvw ⊢ ( 𝑥 = 𝑎 → ( [ 𝑦 / 𝑧 ] [ 𝑦 / 𝑤 ] [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 ) ↔ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) ) → ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 ) ) )
56 7 sbt ⊢ [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 )
57 56 sbt ⊢ [ 𝑦 / 𝑤 ] [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 )
58 57 sbt ⊢ [ 𝑦 / 𝑧 ] [ 𝑦 / 𝑤 ] [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 )
59 55 58 chvarvv ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) ) → ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 )
60 18 21 20 25 59 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) ∧ ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) ) → ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 )
61 60 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) → ( ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) → ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 ) )
62 61 exlimdvv ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) → ( ∃ 𝑔 ∃ 𝑘 ( 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) → ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 ) )
63 17 62 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) → ( ( ∃ 𝑔 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) ∧ ∃ 𝑘 𝑘 ∈ ( 𝑦 𝐻 𝑦 ) ) → ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 ) )
64 14 16 63 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑎 𝐻 𝑦 ) ) ) → ( 1 ( ⟨ 𝑎 , 𝑦 ⟩ · 𝑦 ) 𝑟 ) = 𝑟 )
65 11 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) → ( 𝑦 𝐻 𝑦 ) ≠ ∅ )
66 n0 ⊢ ( ( 𝑦 𝐻 𝑦 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) )
67 65 66 sylib ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) → ∃ 𝑓 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) )
68 id ⊢ ( 𝑦 = 𝑎 → 𝑦 = 𝑎 )
69 68 68 oveq12d ⊢ ( 𝑦 = 𝑎 → ( 𝑦 𝐻 𝑦 ) = ( 𝑎 𝐻 𝑎 ) )
70 69 neeq1d ⊢ ( 𝑦 = 𝑎 → ( ( 𝑦 𝐻 𝑦 ) ≠ ∅ ↔ ( 𝑎 𝐻 𝑎 ) ≠ ∅ ) )
71 11 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝐻 𝑦 ) ≠ ∅ )
72 71 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝐻 𝑦 ) ≠ ∅ )
73 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) → 𝑎 ∈ 𝐵 )
74 70 72 73 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) → ( 𝑎 𝐻 𝑎 ) ≠ ∅ )
75 n0 ⊢ ( ( 𝑎 𝐻 𝑎 ) ≠ ∅ ↔ ∃ 𝑘 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) )
76 74 75 sylib ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) → ∃ 𝑘 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) )
77 exdistrv ⊢ ( ∃ 𝑓 ∃ 𝑘 ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ↔ ( ∃ 𝑓 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ ∃ 𝑘 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) )
78 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) → 𝜑 )
79 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) → 𝑦 ∈ 𝐵 )
80 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) → 𝑎 ∈ 𝐵 )
81 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) → 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) )
82 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) → 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) )
83 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) → 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) )
84 81 82 83 3jca ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) → ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) )
85 simplll ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → 𝑥 = 𝑦 )
86 85 eleq1d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
87 86 anbi1d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
88 87 34 bitrdi ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ 𝑦 ∈ 𝐵 ) )
89 simpllr ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → 𝑧 = 𝑎 )
90 89 eleq1d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝑧 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵 ) )
91 simplr ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → 𝑤 = 𝑎 )
92 91 eleq1d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝑤 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵 ) )
93 90 92 anbi12d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ↔ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ) )
94 anidm ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ↔ 𝑎 ∈ 𝐵 )
95 93 94 bitrdi ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ↔ 𝑎 ∈ 𝐵 ) )
96 85 oveq1d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑦 ) )
97 96 eleq2d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ) )
98 simpr ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → 𝑔 = 𝑟 )
99 89 oveq2d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑦 𝐻 𝑎 ) )
100 98 99 eleq12d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ↔ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) )
101 89 91 oveq12d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝑧 𝐻 𝑤 ) = ( 𝑎 𝐻 𝑎 ) )
102 101 eleq2d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ↔ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) )
103 97 100 102 3anbi123d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) )
104 88 95 103 3anbi123d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) ) )
105 5 104 bitrid ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝜓 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) ) )
106 105 anbi2d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) ) ) )
107 89 oveq2d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) )
108 eqidd ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → 1 = 1 )
109 107 98 108 oveq123d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) )
110 109 98 eqeq12d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 ↔ ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 ) )
111 106 110 imbi12d ⊢ ( ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) ∧ 𝑔 = 𝑟 ) → ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) ) → ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 ) ) )
112 111 sbiedvw ⊢ ( ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) ∧ 𝑤 = 𝑎 ) → ( [ 𝑟 / 𝑔 ] ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) ) → ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 ) ) )
113 112 sbiedvw ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑎 ) → ( [ 𝑎 / 𝑤 ] [ 𝑟 / 𝑔 ] ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) ) → ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 ) ) )
114 113 sbiedvw ⊢ ( 𝑥 = 𝑦 → ( [ 𝑎 / 𝑧 ] [ 𝑎 / 𝑤 ] [ 𝑟 / 𝑔 ] ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) ) → ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 ) ) )
115 8 sbt ⊢ [ 𝑟 / 𝑔 ] ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 )
116 115 sbt ⊢ [ 𝑎 / 𝑤 ] [ 𝑟 / 𝑔 ] ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 )
117 116 sbt ⊢ [ 𝑎 / 𝑧 ] [ 𝑎 / 𝑤 ] [ 𝑟 / 𝑔 ] ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 )
118 114 117 chvarvv ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) ) → ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 )
119 78 79 80 84 118 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) ∧ ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) ) → ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 )
120 119 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) → ( ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) → ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 ) )
121 120 exlimdvv ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) → ( ∃ 𝑓 ∃ 𝑘 ( 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) → ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 ) )
122 77 121 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) → ( ( ∃ 𝑓 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) ∧ ∃ 𝑘 𝑘 ∈ ( 𝑎 𝐻 𝑎 ) ) → ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 ) )
123 67 76 122 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) ) → ( 𝑟 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑎 ) 1 ) = 𝑟 )
124 id ⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 )
125 124 124 oveq12d ⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝐻 𝑦 ) = ( 𝑧 𝐻 𝑧 ) )
126 125 neeq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 𝐻 𝑦 ) ≠ ∅ ↔ ( 𝑧 𝐻 𝑧 ) ≠ ∅ ) )
127 71 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝐻 𝑦 ) ≠ ∅ )
128 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
129 126 127 128 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ) → ( 𝑧 𝐻 𝑧 ) ≠ ∅ )
130 n0 ⊢ ( ( 𝑧 𝐻 𝑧 ) ≠ ∅ ↔ ∃ 𝑘 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) )
131 129 130 sylib ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ) → ∃ 𝑘 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) )
132 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
133 132 3anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) )
134 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐻 𝑎 ) = ( 𝑦 𝐻 𝑎 ) )
135 134 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ↔ 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ) )
136 135 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ↔ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ) )
137 136 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ↔ ( ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) )
138 133 137 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) )
139 138 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) ↔ ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) ) )
140 opeq1 ⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑎 ⟩ = ⟨ 𝑦 , 𝑎 ⟩ )
141 140 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) = ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) )
142 141 oveqd ⊢ ( 𝑥 = 𝑦 → ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) )
143 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐻 𝑧 ) = ( 𝑦 𝐻 𝑧 ) )
144 142 143 eleq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑥 𝐻 𝑧 ) ↔ ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑦 𝐻 𝑧 ) ) )
145 139 144 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑦 𝐻 𝑧 ) ) ) )
146 df-3an ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
147 5 146 bitri ⊢ ( 𝜓 ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
148 simpll ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → 𝑦 = 𝑎 )
149 148 eleq1d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵 ) )
150 149 anbi2d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ) )
151 simplr ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → 𝑤 = 𝑧 )
152 151 eleq1d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( 𝑤 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
153 152 anbi2d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) )
154 anidm ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ↔ 𝑧 ∈ 𝐵 )
155 153 154 bitrdi ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ↔ 𝑧 ∈ 𝐵 ) )
156 150 155 anbi12d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) ) )
157 df-3an ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) )
158 156 157 bitr4di ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) )
159 simpr ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → 𝑓 = 𝑟 )
160 148 oveq2d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐻 𝑎 ) )
161 159 160 eleq12d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ) )
162 148 oveq1d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑎 𝐻 𝑧 ) )
163 162 eleq2d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ↔ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) )
164 151 oveq2d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( 𝑧 𝐻 𝑤 ) = ( 𝑧 𝐻 𝑧 ) )
165 164 eleq2d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ↔ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) )
166 161 163 165 3anbi123d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) )
167 df-3an ⊢ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ↔ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) )
168 166 167 bitrdi ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) )
169 158 168 anbi12d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) )
170 147 169 bitrid ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( 𝜓 ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) )
171 170 anbi2d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) ) )
172 148 opeq2d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ )
173 172 oveq1d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) )
174 eqidd ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → 𝑔 = 𝑔 )
175 173 174 159 oveq123d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) )
176 175 eleq1d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ↔ ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑥 𝐻 𝑧 ) ) )
177 171 176 imbi12d ⊢ ( ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) ∧ 𝑓 = 𝑟 ) → ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ) )
178 177 sbiedvw ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑤 = 𝑧 ) → ( [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ) )
179 178 sbiedvw ⊢ ( 𝑦 = 𝑎 → ( [ 𝑧 / 𝑤 ] [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ) )
180 9 sbt ⊢ [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
181 180 sbt ⊢ [ 𝑧 / 𝑤 ] [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
182 179 181 chvarvv ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑥 𝐻 𝑧 ) )
183 145 182 chvarvv ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑦 𝐻 𝑧 ) )
184 183 exp45 ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) → ( 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑦 𝐻 𝑧 ) ) ) ) )
185 184 3imp ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ) → ( 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑦 𝐻 𝑧 ) ) )
186 185 exlimdv ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ) → ( ∃ 𝑘 𝑘 ∈ ( 𝑧 𝐻 𝑧 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑦 𝐻 𝑧 ) ) )
187 131 186 mpd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ∈ ( 𝑦 𝐻 𝑧 ) )
188 132 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ) )
189 188 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) )
190 135 3anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
191 189 190 3anbi23d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) )
192 140 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑤 ) = ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑤 ) )
193 192 oveqd ⊢ ( 𝑥 = 𝑦 → ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) = ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) )
194 opeq1 ⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑧 ⟩ )
195 194 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) = ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) )
196 eqidd ⊢ ( 𝑥 = 𝑦 → 𝑘 = 𝑘 )
197 195 196 142 oveq123d ⊢ ( 𝑥 = 𝑦 → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) = ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) )
198 193 197 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) ↔ ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) = ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) ) )
199 191 198 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) = ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) ) ) )
200 simpl ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → 𝑦 = 𝑎 )
201 200 eleq1d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵 ) )
202 201 anbi2d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ) )
203 simpr ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → 𝑓 = 𝑟 )
204 200 oveq2d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐻 𝑎 ) )
205 203 204 eleq12d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ) )
206 200 oveq1d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑎 𝐻 𝑧 ) )
207 206 eleq2d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ↔ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ) )
208 205 207 3anbi12d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
209 202 208 3anbi13d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) )
210 5 209 bitrid ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( 𝜓 ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) )
211 df-3an ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
212 210 211 bitrdi ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( 𝜓 ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) )
213 212 anbi2d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) ) )
214 3anass ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) )
215 213 214 bitr4di ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) )
216 200 opeq2d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ )
217 216 oveq1d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) = ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑤 ) )
218 200 opeq1d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑎 , 𝑧 ⟩ )
219 218 oveq1d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) = ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) )
220 219 oveqd ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) = ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) )
221 217 220 203 oveq123d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) )
222 216 oveq1d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) )
223 eqidd ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → 𝑔 = 𝑔 )
224 222 223 203 oveq123d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) )
225 224 oveq2d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) )
226 221 225 eqeq12d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ↔ ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) ) )
227 215 226 imbi12d ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑓 = 𝑟 ) → ( ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) ) ) )
228 227 sbiedvw ⊢ ( 𝑦 = 𝑎 → ( [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) ) ) )
229 10 sbt ⊢ [ 𝑟 / 𝑓 ] ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
230 228 229 chvarvv ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑥 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) )
231 199 230 chvarvv ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑟 ∈ ( 𝑦 𝐻 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( ( 𝑘 ( ⟨ 𝑎 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑤 ) 𝑟 ) = ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑦 , 𝑎 ⟩ · 𝑧 ) 𝑟 ) ) )
232 1 2 3 4 6 64 123 187 231 iscatd ⊢ ( 𝜑 → 𝐶 ∈ Cat )
233 1 2 3 232 6 64 123 catidd ⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 1 ) )
234 232 233 jca ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 1 ) ) )