Metamath Proof Explorer

Theorem dihjatcclem4

Description: Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 29-Sep-2014)

Ref Expression
Hypotheses dihjatcclem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihjatcclem.l ⊢ ≤ = ( le ‘ 𝐾 )
dihjatcclem.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihjatcclem.j ⊢ ∨ = ( join ‘ 𝐾 )
dihjatcclem.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihjatcclem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihjatcclem.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihjatcclem.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dihjatcclem.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihjatcclem.v ⊢ 𝑉 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
dihjatcclem.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihjatcclem.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
dihjatcclem.q ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
dihjatcc.w ⊢ 𝐶 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihjatcc.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihjatcc.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dihjatcc.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihjatcc.g ⊢ 𝐺 = ( ℩ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝐶 ) = 𝑃 )
dihjatcc.dd ⊢ 𝐷 = ( ℩ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝐶 ) = 𝑄 )
dihjatcc.n ⊢ 𝑁 = ( 𝑎 ∈ 𝐸 ↦ ( 𝑑 ∈ 𝑇 ↦ ◡ ( 𝑎 ‘ 𝑑 ) ) )
dihjatcc.o ⊢ 0 = ( 𝑑 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
dihjatcc.d ⊢ 𝐽 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑑 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑑 ) ∘ ( 𝑏 ‘ 𝑑 ) ) ) )
Assertion dihjatcclem4 ( 𝜑 → ( 𝐼 ‘ 𝑉 ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 dihjatcclem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihjatcclem.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihjatcclem.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihjatcclem.j ⊢ ∨ = ( join ‘ 𝐾 )
5 dihjatcclem.m ⊢ ∧ = ( meet ‘ 𝐾 )
6 dihjatcclem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7 dihjatcclem.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8 dihjatcclem.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
9 dihjatcclem.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
10 dihjatcclem.v ⊢ 𝑉 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
11 dihjatcclem.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 dihjatcclem.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
13 dihjatcclem.q ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
14 dihjatcc.w ⊢ 𝐶 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
15 dihjatcc.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
16 dihjatcc.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
17 dihjatcc.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
18 dihjatcc.g ⊢ 𝐺 = ( ℩ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝐶 ) = 𝑃 )
19 dihjatcc.dd ⊢ 𝐷 = ( ℩ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝐶 ) = 𝑄 )
20 dihjatcc.n ⊢ 𝑁 = ( 𝑎 ∈ 𝐸 ↦ ( 𝑑 ∈ 𝑇 ↦ ◡ ( 𝑎 ‘ 𝑑 ) ) )
21 dihjatcc.o ⊢ 0 = ( 𝑑 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
22 dihjatcc.d ⊢ 𝐽 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑑 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑑 ) ∘ ( 𝑏 ‘ 𝑑 ) ) ) )
23 3 9 dihvalrel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑉 ) )
24 11 23 syl ⊢ ( 𝜑 → Rel ( 𝐼 ‘ 𝑉 ) )
25 11 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
26 2 6 3 14 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊 ) )
27 11 26 syl ⊢ ( 𝜑 → ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊 ) )
28 2 6 3 15 18 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
29 11 27 12 28 syl3anc ⊢ ( 𝜑 → 𝐺 ∈ 𝑇 )
30 2 6 3 15 19 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐷 ∈ 𝑇 )
31 11 27 13 30 syl3anc ⊢ ( 𝜑 → 𝐷 ∈ 𝑇 )
32 3 15 ltrncnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐷 ∈ 𝑇 ) → ◡ 𝐷 ∈ 𝑇 )
33 11 31 32 syl2anc ⊢ ( 𝜑 → ◡ 𝐷 ∈ 𝑇 )
34 3 15 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ◡ 𝐷 ∈ 𝑇 ) → ( 𝐺 ∘ ◡ 𝐷 ) ∈ 𝑇 )
35 11 29 33 34 syl3anc ⊢ ( 𝜑 → ( 𝐺 ∘ ◡ 𝐷 ) ∈ 𝑇 )
36 35 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ( 𝐺 ∘ ◡ 𝐷 ) ∈ 𝑇 )
37 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → 𝑓 ∈ 𝑇 )
38 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 )
39 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 dihjatcclem3 ⊢ ( 𝜑 → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑉 )
40 39 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑉 )
41 38 40 breqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) )
42 2 3 15 16 17 tendoex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐺 ∘ ◡ 𝐷 ) ∈ 𝑇 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) → ∃ 𝑡 ∈ 𝐸 ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 )
43 25 36 37 41 42 syl121anc ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ∃ 𝑡 ∈ 𝐸 ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 )
44 df-rex ⊢ ( ∃ 𝑡 ∈ 𝐸 ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ↔ ∃ 𝑡 ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) )
45 43 44 sylib ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ∃ 𝑡 ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) )
46 eqidd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( 𝑡 ‘ 𝐺 ) = ( 𝑡 ‘ 𝐺 ) )
47 simprl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → 𝑡 ∈ 𝐸 )
48 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
49 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
50 fvex ⊢ ( 𝑡 ‘ 𝐺 ) ∈ V
51 vex ⊢ 𝑡 ∈ V
52 2 6 3 14 15 17 9 18 50 51 dihopelvalcqat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ↔ ( ( 𝑡 ‘ 𝐺 ) = ( 𝑡 ‘ 𝐺 ) ∧ 𝑡 ∈ 𝐸 ) ) )
53 48 49 52 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ↔ ( ( 𝑡 ‘ 𝐺 ) = ( 𝑡 ‘ 𝐺 ) ∧ 𝑡 ∈ 𝐸 ) ) )
54 46 47 53 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) )
55 eqidd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) )
56 3 15 17 20 tendoicl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ) → ( 𝑁 ‘ 𝑡 ) ∈ 𝐸 )
57 48 47 56 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( 𝑁 ‘ 𝑡 ) ∈ 𝐸 )
58 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
59 fvex ⊢ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ∈ V
60 fvex ⊢ ( 𝑁 ‘ 𝑡 ) ∈ V
61 2 6 3 14 15 17 9 19 59 60 dihopelvalcqat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , ( 𝑁 ‘ 𝑡 ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ∧ ( 𝑁 ‘ 𝑡 ) ∈ 𝐸 ) ) )
62 48 58 61 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , ( 𝑁 ‘ 𝑡 ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ∧ ( 𝑁 ‘ 𝑡 ) ∈ 𝐸 ) ) )
63 55 57 62 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , ( 𝑁 ‘ 𝑡 ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) )
64 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → 𝐺 ∈ 𝑇 )
65 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ◡ 𝐷 ∈ 𝑇 )
66 3 15 17 tendospdi1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ∧ ◡ 𝐷 ∈ 𝑇 ) ) → ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = ( ( 𝑡 ‘ 𝐺 ) ∘ ( 𝑡 ‘ ◡ 𝐷 ) ) )
67 48 47 64 65 66 syl13anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = ( ( 𝑡 ‘ 𝐺 ) ∘ ( 𝑡 ‘ ◡ 𝐷 ) ) )
68 simprr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 )
69 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → 𝐷 ∈ 𝑇 )
70 20 15 tendoi2 ⊢ ( ( 𝑡 ∈ 𝐸 ∧ 𝐷 ∈ 𝑇 ) → ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) = ◡ ( 𝑡 ‘ 𝐷 ) )
71 47 69 70 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) = ◡ ( 𝑡 ‘ 𝐷 ) )
72 3 15 17 tendocnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ∧ 𝐷 ∈ 𝑇 ) → ◡ ( 𝑡 ‘ 𝐷 ) = ( 𝑡 ‘ ◡ 𝐷 ) )
73 48 47 69 72 syl3anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ◡ ( 𝑡 ‘ 𝐷 ) = ( 𝑡 ‘ ◡ 𝐷 ) )
74 71 73 eqtr2d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( 𝑡 ‘ ◡ 𝐷 ) = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) )
75 74 coeq2d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( ( 𝑡 ‘ 𝐺 ) ∘ ( 𝑡 ‘ ◡ 𝐷 ) ) = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) )
76 67 68 75 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) )
77 simplrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → 𝑠 = 0 )
78 3 15 17 20 1 22 21 tendoipl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ) → ( 𝑡 𝐽 ( 𝑁 ‘ 𝑡 ) ) = 0 )
79 48 47 78 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ( 𝑡 𝐽 ( 𝑁 ‘ 𝑡 ) ) = 0 )
80 77 79 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → 𝑠 = ( 𝑡 𝐽 ( 𝑁 ‘ 𝑡 ) ) )
81 opeq1 ⊢ ( 𝑔 = ( 𝑡 ‘ 𝐺 ) → ⟨ 𝑔 , 𝑡 ⟩ = ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ )
82 81 eleq1d ⊢ ( 𝑔 = ( 𝑡 ‘ 𝐺 ) → ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ↔ ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ) )
83 82 anbi1d ⊢ ( 𝑔 = ( 𝑡 ‘ 𝐺 ) → ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ↔ ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ) )
84 coeq1 ⊢ ( 𝑔 = ( 𝑡 ‘ 𝐺 ) → ( 𝑔 ∘ ℎ ) = ( ( 𝑡 ‘ 𝐺 ) ∘ ℎ ) )
85 84 eqeq2d ⊢ ( 𝑔 = ( 𝑡 ‘ 𝐺 ) → ( 𝑓 = ( 𝑔 ∘ ℎ ) ↔ 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ℎ ) ) )
86 85 anbi1d ⊢ ( 𝑔 = ( 𝑡 ‘ 𝐺 ) → ( ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ↔ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) )
87 83 86 anbi12d ⊢ ( 𝑔 = ( 𝑡 ‘ 𝐺 ) → ( ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ↔ ( ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ) )
88 opeq1 ⊢ ( ℎ = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) → ⟨ ℎ , 𝑢 ⟩ = ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , 𝑢 ⟩ )
89 88 eleq1d ⊢ ( ℎ = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) → ( ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) )
90 89 anbi2d ⊢ ( ℎ = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) → ( ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ↔ ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ) )
91 coeq2 ⊢ ( ℎ = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) → ( ( 𝑡 ‘ 𝐺 ) ∘ ℎ ) = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) )
92 91 eqeq2d ⊢ ( ℎ = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) → ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ℎ ) ↔ 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) ) )
93 92 anbi1d ⊢ ( ℎ = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) → ( ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ↔ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) )
94 90 93 anbi12d ⊢ ( ℎ = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) → ( ( ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ↔ ( ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ) )
95 opeq2 ⊢ ( 𝑢 = ( 𝑁 ‘ 𝑡 ) → ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , 𝑢 ⟩ = ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , ( 𝑁 ‘ 𝑡 ) ⟩ )
96 95 eleq1d ⊢ ( 𝑢 = ( 𝑁 ‘ 𝑡 ) → ( ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , ( 𝑁 ‘ 𝑡 ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) )
97 96 anbi2d ⊢ ( 𝑢 = ( 𝑁 ‘ 𝑡 ) → ( ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ↔ ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , ( 𝑁 ‘ 𝑡 ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ) )
98 oveq2 ⊢ ( 𝑢 = ( 𝑁 ‘ 𝑡 ) → ( 𝑡 𝐽 𝑢 ) = ( 𝑡 𝐽 ( 𝑁 ‘ 𝑡 ) ) )
99 98 eqeq2d ⊢ ( 𝑢 = ( 𝑁 ‘ 𝑡 ) → ( 𝑠 = ( 𝑡 𝐽 𝑢 ) ↔ 𝑠 = ( 𝑡 𝐽 ( 𝑁 ‘ 𝑡 ) ) ) )
100 99 anbi2d ⊢ ( 𝑢 = ( 𝑁 ‘ 𝑡 ) → ( ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ↔ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) ∧ 𝑠 = ( 𝑡 𝐽 ( 𝑁 ‘ 𝑡 ) ) ) ) )
101 97 100 anbi12d ⊢ ( 𝑢 = ( 𝑁 ‘ 𝑡 ) → ( ( ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ↔ ( ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , ( 𝑁 ‘ 𝑡 ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) ∧ 𝑠 = ( 𝑡 𝐽 ( 𝑁 ‘ 𝑡 ) ) ) ) ) )
102 87 94 101 syl3an9b ⊢ ( ( 𝑔 = ( 𝑡 ‘ 𝐺 ) ∧ ℎ = ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ∧ 𝑢 = ( 𝑁 ‘ 𝑡 ) ) → ( ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ↔ ( ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , ( 𝑁 ‘ 𝑡 ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) ∧ 𝑠 = ( 𝑡 𝐽 ( 𝑁 ‘ 𝑡 ) ) ) ) ) )
103 102 spc3egv ⊢ ( ( ( 𝑡 ‘ 𝐺 ) ∈ V ∧ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ∈ V ∧ ( 𝑁 ‘ 𝑡 ) ∈ V ) → ( ( ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , ( 𝑁 ‘ 𝑡 ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) ∧ 𝑠 = ( 𝑡 𝐽 ( 𝑁 ‘ 𝑡 ) ) ) ) → ∃ 𝑔 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ) )
104 50 59 60 103 mp3an ⊢ ( ( ( ⟨ ( 𝑡 ‘ 𝐺 ) , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) , ( 𝑁 ‘ 𝑡 ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( ( 𝑡 ‘ 𝐺 ) ∘ ( ( 𝑁 ‘ 𝑡 ) ‘ 𝐷 ) ) ∧ 𝑠 = ( 𝑡 𝐽 ( 𝑁 ‘ 𝑡 ) ) ) ) → ∃ 𝑔 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) )
105 54 63 76 80 104 syl22anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) ) → ∃ 𝑔 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) )
106 105 ex ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ( ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) → ∃ 𝑔 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ) )
107 106 eximdv ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ( ∃ 𝑡 ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) → ∃ 𝑡 ∃ 𝑔 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ) )
108 excom ⊢ ( ∃ 𝑡 ∃ 𝑔 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ↔ ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) )
109 107 108 imbitrdi ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ( ∃ 𝑡 ( 𝑡 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑓 ) → ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ) )
110 45 109 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) → ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) )
111 110 ex ⊢ ( 𝜑 → ( ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) → ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ) )
112 11 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
113 112 hllatd ⊢ ( 𝜑 → 𝐾 ∈ Lat )
114 12 simpld ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
115 13 simpld ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
116 1 4 6 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
117 112 114 115 116 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
118 11 simprd ⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
119 1 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
120 118 119 syl ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
121 1 5 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ 𝐵 )
122 113 117 120 121 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ 𝐵 )
123 10 122 eqeltrid ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
124 1 2 5 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
125 113 117 120 124 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
126 10 125 eqbrtrid ⊢ ( 𝜑 → 𝑉 ≤ 𝑊 )
127 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
128 1 2 3 9 127 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑉 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) )
129 11 123 126 128 syl12anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑉 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) )
130 129 eleq2d ⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑉 ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) ) )
131 1 2 3 15 16 21 127 dibopelval3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑉 ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) )
132 11 123 126 131 syl12anc ⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑉 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) )
133 130 132 bitrd ⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑉 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ) ∧ 𝑠 = 0 ) ) )
134 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
135 1 6 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
136 114 135 syl ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
137 1 6 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
138 115 137 syl ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
139 1 3 15 17 22 7 134 8 9 11 136 138 dihopellsm ⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) ↔ ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ) ∧ ( 𝑓 = ( 𝑔 ∘ ℎ ) ∧ 𝑠 = ( 𝑡 𝐽 𝑢 ) ) ) ) )
140 111 133 139 3imtr4d ⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑉 ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) ) )
141 24 140 relssdv ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑉 ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )