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