Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihjatcclem4 Structured version   Visualization version   GIF version

Theorem dihjatcclem4 38987
 Description: Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 29-Sep-2014.)
Hypotheses
Ref Expression
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
Ref Expression
dihjatcclem4 (𝜑 → (𝐼𝑉) ⊆ ((𝐼𝑃) (𝐼𝑄)))
Distinct variable groups:   ,𝑑   𝐴,𝑑   𝐵,𝑑   𝐶,𝑑   𝑎,𝑏,𝐸   𝐻,𝑑   𝑃,𝑑   𝑎,𝑑,𝐾,𝑏   𝑄,𝑑   𝑇,𝑎,𝑏,𝑑   𝑊,𝑎,𝑏,𝑑
Allowed substitution hints:   𝜑(𝑎,𝑏,𝑑)   𝐴(𝑎,𝑏)   𝐵(𝑎,𝑏)   𝐶(𝑎,𝑏)   𝐷(𝑎,𝑏,𝑑)   𝑃(𝑎,𝑏)   (𝑎,𝑏,𝑑)   𝑄(𝑎,𝑏)   𝑅(𝑎,𝑏,𝑑)   𝑈(𝑎,𝑏,𝑑)   𝐸(𝑑)   𝐺(𝑎,𝑏,𝑑)   𝐻(𝑎,𝑏)   𝐼(𝑎,𝑏,𝑑)   𝐽(𝑎,𝑏,𝑑)   (𝑎,𝑏,𝑑)   (𝑎,𝑏)   (𝑎,𝑏,𝑑)   𝑁(𝑎,𝑏,𝑑)   𝑉(𝑎,𝑏,𝑑)   0 (𝑎,𝑏,𝑑)

Proof of Theorem dihjatcclem4
Dummy variables 𝑡 𝑓 𝑠 𝑔 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dihjatcclem.k . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 dihjatcclem.h . . . 4 𝐻 = (LHyp‘𝐾)
3 dihjatcclem.i . . . 4 𝐼 = ((DIsoH‘𝐾)‘𝑊)
42, 3dihvalrel 38845 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → Rel (𝐼𝑉))
51, 4syl 17 . 2 (𝜑 → Rel (𝐼𝑉))
61adantr 485 . . . . . . 7 ((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) → (𝐾 ∈ HL ∧ 𝑊𝐻))
7 dihjatcclem.l . . . . . . . . . . . 12 = (le‘𝐾)
8 dihjatcclem.a . . . . . . . . . . . 12 𝐴 = (Atoms‘𝐾)
9 dihjatcc.w . . . . . . . . . . . 12 𝐶 = ((oc‘𝐾)‘𝑊)
107, 8, 2, 9lhpocnel2 37585 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝐶𝐴 ∧ ¬ 𝐶 𝑊))
111, 10syl 17 . . . . . . . . . 10 (𝜑 → (𝐶𝐴 ∧ ¬ 𝐶 𝑊))
12 dihjatcclem.p . . . . . . . . . 10 (𝜑 → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
13 dihjatcc.t . . . . . . . . . . 11 𝑇 = ((LTrn‘𝐾)‘𝑊)
14 dihjatcc.g . . . . . . . . . . 11 𝐺 = (𝑑𝑇 (𝑑𝐶) = 𝑃)
157, 8, 2, 13, 14ltrniotacl 38145 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐶𝐴 ∧ ¬ 𝐶 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐺𝑇)
161, 11, 12, 15syl3anc 1369 . . . . . . . . 9 (𝜑𝐺𝑇)
17 dihjatcclem.q . . . . . . . . . . 11 (𝜑 → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
18 dihjatcc.dd . . . . . . . . . . . 12 𝐷 = (𝑑𝑇 (𝑑𝐶) = 𝑄)
197, 8, 2, 13, 18ltrniotacl 38145 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐶𝐴 ∧ ¬ 𝐶 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → 𝐷𝑇)
201, 11, 17, 19syl3anc 1369 . . . . . . . . . 10 (𝜑𝐷𝑇)
212, 13ltrncnv 37712 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐷𝑇) → 𝐷𝑇)
221, 20, 21syl2anc 588 . . . . . . . . 9 (𝜑𝐷𝑇)
232, 13ltrnco 38285 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇𝐷𝑇) → (𝐺𝐷) ∈ 𝑇)
241, 16, 22, 23syl3anc 1369 . . . . . . . 8 (𝜑 → (𝐺𝐷) ∈ 𝑇)
2524adantr 485 . . . . . . 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‘𝐾)‘𝑊)
3628, 7, 2, 29, 30, 8, 31, 32, 3, 33, 1, 12, 17, 9, 13, 34, 35, 14, 18dihjatcclem3 38986 . . . . . . . . 9 (𝜑 → (𝑅‘(𝐺𝐷)) = 𝑉)
3736adantr 485 . . . . . . . 8 ((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) → (𝑅‘(𝐺𝐷)) = 𝑉)
3827, 37breqtrrd 5058 . . . . . . 7 ((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) → (𝑅𝑓) (𝑅‘(𝐺𝐷)))
397, 2, 13, 34, 35tendoex 38541 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐺𝐷) ∈ 𝑇𝑓𝑇) ∧ (𝑅𝑓) (𝑅‘(𝐺𝐷))) → ∃𝑡𝐸 (𝑡‘(𝐺𝐷)) = 𝑓)
406, 25, 26, 38, 39syl121anc 1373 . . . . . 6 ((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) → ∃𝑡𝐸 (𝑡‘(𝐺𝐷)) = 𝑓)
41 df-rex 3077 . . . . . 6 (∃𝑡𝐸 (𝑡‘(𝐺𝐷)) = 𝑓 ↔ ∃𝑡(𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓))
4240, 41sylib 221 . . . . 5 ((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) → ∃𝑡(𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓))
43 eqidd 2760 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (𝑡𝐺) = (𝑡𝐺))
44 simprl 771 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → 𝑡𝐸)
451ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
4612ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
47 fvex 6669 . . . . . . . . . . . 12 (𝑡𝐺) ∈ V
48 vex 3414 . . . . . . . . . . . 12 𝑡 ∈ V
497, 8, 2, 9, 13, 35, 3, 14, 47, 48dihopelvalcqat 38812 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ↔ ((𝑡𝐺) = (𝑡𝐺) ∧ 𝑡𝐸)))
5045, 46, 49syl2anc 588 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ↔ ((𝑡𝐺) = (𝑡𝐺) ∧ 𝑡𝐸)))
5143, 44, 50mpbir2and 713 . . . . . . . . 9 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → ⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃))
52 eqidd 2760 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → ((𝑁𝑡)‘𝐷) = ((𝑁𝑡)‘𝐷))
53 dihjatcc.n . . . . . . . . . . . 12 𝑁 = (𝑎𝐸 ↦ (𝑑𝑇(𝑎𝑑)))
542, 13, 35, 53tendoicl 38362 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸) → (𝑁𝑡) ∈ 𝐸)
5545, 44, 54syl2anc 588 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (𝑁𝑡) ∈ 𝐸)
5617ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
57 fvex 6669 . . . . . . . . . . . 12 ((𝑁𝑡)‘𝐷) ∈ V
58 fvex 6669 . . . . . . . . . . . 12 (𝑁𝑡) ∈ V
597, 8, 2, 9, 13, 35, 3, 18, 57, 58dihopelvalcqat 38812 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (⟨((𝑁𝑡)‘𝐷), (𝑁𝑡)⟩ ∈ (𝐼𝑄) ↔ (((𝑁𝑡)‘𝐷) = ((𝑁𝑡)‘𝐷) ∧ (𝑁𝑡) ∈ 𝐸)))
6045, 56, 59syl2anc 588 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (⟨((𝑁𝑡)‘𝐷), (𝑁𝑡)⟩ ∈ (𝐼𝑄) ↔ (((𝑁𝑡)‘𝐷) = ((𝑁𝑡)‘𝐷) ∧ (𝑁𝑡) ∈ 𝐸)))
6152, 55, 60mpbir2and 713 . . . . . . . . 9 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → ⟨((𝑁𝑡)‘𝐷), (𝑁𝑡)⟩ ∈ (𝐼𝑄))
6216ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → 𝐺𝑇)
6322ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → 𝐷𝑇)
642, 13, 35tendospdi1 38586 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐸𝐺𝑇𝐷𝑇)) → (𝑡‘(𝐺𝐷)) = ((𝑡𝐺) ∘ (𝑡𝐷)))
6545, 44, 62, 63, 64syl13anc 1370 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (𝑡‘(𝐺𝐷)) = ((𝑡𝐺) ∘ (𝑡𝐷)))
66 simprr 773 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (𝑡‘(𝐺𝐷)) = 𝑓)
6720ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → 𝐷𝑇)
6853, 13tendoi2 38361 . . . . . . . . . . . . 13 ((𝑡𝐸𝐷𝑇) → ((𝑁𝑡)‘𝐷) = (𝑡𝐷))
6944, 67, 68syl2anc 588 . . . . . . . . . . . 12 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → ((𝑁𝑡)‘𝐷) = (𝑡𝐷))
702, 13, 35tendocnv 38587 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸𝐷𝑇) → (𝑡𝐷) = (𝑡𝐷))
7145, 44, 67, 70syl3anc 1369 . . . . . . . . . . . 12 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (𝑡𝐷) = (𝑡𝐷))
7269, 71eqtr2d 2795 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (𝑡𝐷) = ((𝑁𝑡)‘𝐷))
7372coeq2d 5700 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → ((𝑡𝐺) ∘ (𝑡𝐷)) = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)))
7465, 66, 733eqtr3d 2802 . . . . . . . . 9 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → 𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)))
75 simplrr 778 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → 𝑠 = 0 )
76 dihjatcc.d . . . . . . . . . . . 12 𝐽 = (𝑎𝐸, 𝑏𝐸 ↦ (𝑑𝑇 ↦ ((𝑎𝑑) ∘ (𝑏𝑑))))
77 dihjatcc.o . . . . . . . . . . . 12 0 = (𝑑𝑇 ↦ ( I ↾ 𝐵))
782, 13, 35, 53, 28, 76, 77tendoipl2 38364 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸) → (𝑡𝐽(𝑁𝑡)) = 0 )
7945, 44, 78syl2anc 588 . . . . . . . . . 10 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → (𝑡𝐽(𝑁𝑡)) = 0 )
8075, 79eqtr4d 2797 . . . . . . . . 9 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → 𝑠 = (𝑡𝐽(𝑁𝑡)))
81 opeq1 4759 . . . . . . . . . . . . . . 15 (𝑔 = (𝑡𝐺) → ⟨𝑔, 𝑡⟩ = ⟨(𝑡𝐺), 𝑡⟩)
8281eleq1d 2837 . . . . . . . . . . . . . 14 (𝑔 = (𝑡𝐺) → (⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ↔ ⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃)))
8382anbi1d 633 . . . . . . . . . . . . 13 (𝑔 = (𝑡𝐺) → ((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ↔ (⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄))))
84 coeq1 5695 . . . . . . . . . . . . . . 15 (𝑔 = (𝑡𝐺) → (𝑔) = ((𝑡𝐺) ∘ ))
8584eqeq2d 2770 . . . . . . . . . . . . . 14 (𝑔 = (𝑡𝐺) → (𝑓 = (𝑔) ↔ 𝑓 = ((𝑡𝐺) ∘ )))
8685anbi1d 633 . . . . . . . . . . . . 13 (𝑔 = (𝑡𝐺) → ((𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢)) ↔ (𝑓 = ((𝑡𝐺) ∘ ) ∧ 𝑠 = (𝑡𝐽𝑢))))
8783, 86anbi12d 634 . . . . . . . . . . . 12 (𝑔 = (𝑡𝐺) → (((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢))) ↔ ((⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = ((𝑡𝐺) ∘ ) ∧ 𝑠 = (𝑡𝐽𝑢)))))
88 opeq1 4759 . . . . . . . . . . . . . . 15 ( = ((𝑁𝑡)‘𝐷) → ⟨, 𝑢⟩ = ⟨((𝑁𝑡)‘𝐷), 𝑢⟩)
8988eleq1d 2837 . . . . . . . . . . . . . 14 ( = ((𝑁𝑡)‘𝐷) → (⟨, 𝑢⟩ ∈ (𝐼𝑄) ↔ ⟨((𝑁𝑡)‘𝐷), 𝑢⟩ ∈ (𝐼𝑄)))
9089anbi2d 632 . . . . . . . . . . . . 13 ( = ((𝑁𝑡)‘𝐷) → ((⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ↔ (⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨((𝑁𝑡)‘𝐷), 𝑢⟩ ∈ (𝐼𝑄))))
91 coeq2 5696 . . . . . . . . . . . . . . 15 ( = ((𝑁𝑡)‘𝐷) → ((𝑡𝐺) ∘ ) = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)))
9291eqeq2d 2770 . . . . . . . . . . . . . 14 ( = ((𝑁𝑡)‘𝐷) → (𝑓 = ((𝑡𝐺) ∘ ) ↔ 𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷))))
9392anbi1d 633 . . . . . . . . . . . . 13 ( = ((𝑁𝑡)‘𝐷) → ((𝑓 = ((𝑡𝐺) ∘ ) ∧ 𝑠 = (𝑡𝐽𝑢)) ↔ (𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)) ∧ 𝑠 = (𝑡𝐽𝑢))))
9490, 93anbi12d 634 . . . . . . . . . . . 12 ( = ((𝑁𝑡)‘𝐷) → (((⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = ((𝑡𝐺) ∘ ) ∧ 𝑠 = (𝑡𝐽𝑢))) ↔ ((⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨((𝑁𝑡)‘𝐷), 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)) ∧ 𝑠 = (𝑡𝐽𝑢)))))
95 opeq2 4761 . . . . . . . . . . . . . . 15 (𝑢 = (𝑁𝑡) → ⟨((𝑁𝑡)‘𝐷), 𝑢⟩ = ⟨((𝑁𝑡)‘𝐷), (𝑁𝑡)⟩)
9695eleq1d 2837 . . . . . . . . . . . . . 14 (𝑢 = (𝑁𝑡) → (⟨((𝑁𝑡)‘𝐷), 𝑢⟩ ∈ (𝐼𝑄) ↔ ⟨((𝑁𝑡)‘𝐷), (𝑁𝑡)⟩ ∈ (𝐼𝑄)))
9796anbi2d 632 . . . . . . . . . . . . 13 (𝑢 = (𝑁𝑡) → ((⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨((𝑁𝑡)‘𝐷), 𝑢⟩ ∈ (𝐼𝑄)) ↔ (⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨((𝑁𝑡)‘𝐷), (𝑁𝑡)⟩ ∈ (𝐼𝑄))))
98 oveq2 7156 . . . . . . . . . . . . . . 15 (𝑢 = (𝑁𝑡) → (𝑡𝐽𝑢) = (𝑡𝐽(𝑁𝑡)))
9998eqeq2d 2770 . . . . . . . . . . . . . 14 (𝑢 = (𝑁𝑡) → (𝑠 = (𝑡𝐽𝑢) ↔ 𝑠 = (𝑡𝐽(𝑁𝑡))))
10099anbi2d 632 . . . . . . . . . . . . 13 (𝑢 = (𝑁𝑡) → ((𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)) ∧ 𝑠 = (𝑡𝐽𝑢)) ↔ (𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)) ∧ 𝑠 = (𝑡𝐽(𝑁𝑡)))))
10197, 100anbi12d 634 . . . . . . . . . . . 12 (𝑢 = (𝑁𝑡) → (((⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨((𝑁𝑡)‘𝐷), 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)) ∧ 𝑠 = (𝑡𝐽𝑢))) ↔ ((⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨((𝑁𝑡)‘𝐷), (𝑁𝑡)⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)) ∧ 𝑠 = (𝑡𝐽(𝑁𝑡))))))
10287, 94, 101syl3an9b 1432 . . . . . . . . . . 11 ((𝑔 = (𝑡𝐺) ∧ = ((𝑁𝑡)‘𝐷) ∧ 𝑢 = (𝑁𝑡)) → (((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢))) ↔ ((⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨((𝑁𝑡)‘𝐷), (𝑁𝑡)⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)) ∧ 𝑠 = (𝑡𝐽(𝑁𝑡))))))
103102spc3egv 3523 . . . . . . . . . 10 (((𝑡𝐺) ∈ V ∧ ((𝑁𝑡)‘𝐷) ∈ V ∧ (𝑁𝑡) ∈ V) → (((⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨((𝑁𝑡)‘𝐷), (𝑁𝑡)⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)) ∧ 𝑠 = (𝑡𝐽(𝑁𝑡)))) → ∃𝑔𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢)))))
10447, 57, 58, 103mp3an 1459 . . . . . . . . 9 (((⟨(𝑡𝐺), 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨((𝑁𝑡)‘𝐷), (𝑁𝑡)⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = ((𝑡𝐺) ∘ ((𝑁𝑡)‘𝐷)) ∧ 𝑠 = (𝑡𝐽(𝑁𝑡)))) → ∃𝑔𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢))))
10551, 61, 74, 80, 104syl22anc 838 . . . . . . . 8 (((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) ∧ (𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓)) → ∃𝑔𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢))))
106105ex 417 . . . . . . 7 ((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) → ((𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓) → ∃𝑔𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢)))))
107106eximdv 1919 . . . . . 6 ((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) → (∃𝑡(𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓) → ∃𝑡𝑔𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢)))))
108 excom 2167 . . . . . 6 (∃𝑡𝑔𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢))) ↔ ∃𝑔𝑡𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢))))
109107, 108syl6ib 254 . . . . 5 ((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) → (∃𝑡(𝑡𝐸 ∧ (𝑡‘(𝐺𝐷)) = 𝑓) → ∃𝑔𝑡𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢)))))
11042, 109mpd 15 . . . 4 ((𝜑 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )) → ∃𝑔𝑡𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢))))
111110ex 417 . . 3 (𝜑 → (((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 ) → ∃𝑔𝑡𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢)))))
1121simpld 499 . . . . . . . . 9 (𝜑𝐾 ∈ HL)
113112hllatd 36930 . . . . . . . 8 (𝜑𝐾 ∈ Lat)
11412simpld 499 . . . . . . . . 9 (𝜑𝑃𝐴)
11517simpld 499 . . . . . . . . 9 (𝜑𝑄𝐴)
11628, 29, 8hlatjcl 36933 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ 𝐵)
117112, 114, 115, 116syl3anc 1369 . . . . . . . 8 (𝜑 → (𝑃 𝑄) ∈ 𝐵)
1181simprd 500 . . . . . . . . 9 (𝜑𝑊𝐻)
11928, 2lhpbase 37564 . . . . . . . . 9 (𝑊𝐻𝑊𝐵)
120118, 119syl 17 . . . . . . . 8 (𝜑𝑊𝐵)
12128, 30latmcl 17718 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ 𝐵𝑊𝐵) → ((𝑃 𝑄) 𝑊) ∈ 𝐵)
122113, 117, 120, 121syl3anc 1369 . . . . . . 7 (𝜑 → ((𝑃 𝑄) 𝑊) ∈ 𝐵)
12333, 122eqeltrid 2857 . . . . . 6 (𝜑𝑉𝐵)
12428, 7, 30latmle2 17743 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ 𝐵𝑊𝐵) → ((𝑃 𝑄) 𝑊) 𝑊)
125113, 117, 120, 124syl3anc 1369 . . . . . . 7 (𝜑 → ((𝑃 𝑄) 𝑊) 𝑊)
12633, 125eqbrtrid 5065 . . . . . 6 (𝜑𝑉 𝑊)
127 eqid 2759 . . . . . . 7 ((DIsoB‘𝐾)‘𝑊) = ((DIsoB‘𝐾)‘𝑊)
12828, 7, 2, 3, 127dihvalb 38803 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑉𝐵𝑉 𝑊)) → (𝐼𝑉) = (((DIsoB‘𝐾)‘𝑊)‘𝑉))
1291, 123, 126, 128syl12anc 836 . . . . 5 (𝜑 → (𝐼𝑉) = (((DIsoB‘𝐾)‘𝑊)‘𝑉))
130129eleq2d 2838 . . . 4 (𝜑 → (⟨𝑓, 𝑠⟩ ∈ (𝐼𝑉) ↔ ⟨𝑓, 𝑠⟩ ∈ (((DIsoB‘𝐾)‘𝑊)‘𝑉)))
13128, 7, 2, 13, 34, 77, 127dibopelval3 38714 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑉𝐵𝑉 𝑊)) → (⟨𝑓, 𝑠⟩ ∈ (((DIsoB‘𝐾)‘𝑊)‘𝑉) ↔ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )))
1321, 123, 126, 131syl12anc 836 . . . 4 (𝜑 → (⟨𝑓, 𝑠⟩ ∈ (((DIsoB‘𝐾)‘𝑊)‘𝑉) ↔ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )))
133130, 132bitrd 282 . . 3 (𝜑 → (⟨𝑓, 𝑠⟩ ∈ (𝐼𝑉) ↔ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑉) ∧ 𝑠 = 0 )))
134 eqid 2759 . . . 4 (LSubSp‘𝑈) = (LSubSp‘𝑈)
13528, 8atbase 36855 . . . . 5 (𝑃𝐴𝑃𝐵)
136114, 135syl 17 . . . 4 (𝜑𝑃𝐵)
13728, 8atbase 36855 . . . . 5 (𝑄𝐴𝑄𝐵)
138115, 137syl 17 . . . 4 (𝜑𝑄𝐵)
13928, 2, 13, 35, 76, 31, 134, 32, 3, 1, 136, 138dihopellsm 38821 . . 3 (𝜑 → (⟨𝑓, 𝑠⟩ ∈ ((𝐼𝑃) (𝐼𝑄)) ↔ ∃𝑔𝑡𝑢((⟨𝑔, 𝑡⟩ ∈ (𝐼𝑃) ∧ ⟨, 𝑢⟩ ∈ (𝐼𝑄)) ∧ (𝑓 = (𝑔) ∧ 𝑠 = (𝑡𝐽𝑢)))))
140111, 133, 1393imtr4d 298 . 2 (𝜑 → (⟨𝑓, 𝑠⟩ ∈ (𝐼𝑉) → ⟨𝑓, 𝑠⟩ ∈ ((𝐼𝑃) (𝐼𝑄))))
1415, 140relssdv 5628 1 (𝜑 → (𝐼𝑉) ⊆ ((𝐼𝑃) (𝐼𝑄)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112  ∃wrex 3072  Vcvv 3410   ⊆ wss 3859  ⟨cop 4526   class class class wbr 5030   ↦ cmpt 5110   I cid 5427  ◡ccnv 5521   ↾ cres 5524   ∘ ccom 5526  Rel wrel 5527  ‘cfv 6333  ℩crio 7105  (class class class)co 7148   ∈ cmpo 7150  Basecbs 16531  lecple 16620  occoc 16621  joincjn 17610  meetcmee 17611  Latclat 17711  LSSumclsm 18816  LSubSpclss 19761  Atomscatm 36829  HLchlt 36916  LHypclh 37550  LTrncltrn 37667  trLctrl 37724  TEndoctendo 38318  DVecHcdvh 38644  DIsoBcdib 38704  DIsoHcdih 38794 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-cnex 10621  ax-resscn 10622  ax-1cn 10623  ax-icn 10624  ax-addcl 10625  ax-addrcl 10626  ax-mulcl 10627  ax-mulrcl 10628  ax-mulcom 10629  ax-addass 10630  ax-mulass 10631  ax-distr 10632  ax-i2m1 10633  ax-1ne0 10634  ax-1rid 10635  ax-rnegex 10636  ax-rrecex 10637  ax-cnre 10638  ax-pre-lttri 10639  ax-pre-lttrn 10640  ax-pre-ltadd 10641  ax-pre-mulgt0 10642  ax-riotaBAD 36519 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-tp 4525  df-op 4527  df-uni 4797  df-int 4837  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7578  df-1st 7691  df-2nd 7692  df-tpos 7900  df-undef 7947  df-wrecs 7955  df-recs 8016  df-rdg 8054  df-1o 8110  df-oadd 8114  df-er 8297  df-map 8416  df-en 8526  df-dom 8527  df-sdom 8528  df-fin 8529  df-pnf 10705  df-mnf 10706  df-xr 10707  df-ltxr 10708  df-le 10709  df-sub 10900  df-neg 10901  df-nn 11665  df-2 11727  df-3 11728  df-4 11729  df-5 11730  df-6 11731  df-n0 11925  df-z 12011  df-uz 12273  df-fz 12930  df-struct 16533  df-ndx 16534  df-slot 16535  df-base 16537  df-sets 16538  df-ress 16539  df-plusg 16626  df-mulr 16627  df-sca 16629  df-vsca 16630  df-0g 16763  df-proset 17594  df-poset 17612  df-plt 17624  df-lub 17640  df-glb 17641  df-join 17642  df-meet 17643  df-p0 17705  df-p1 17706  df-lat 17712  df-clat 17774  df-mgm 17908  df-sgrp 17957  df-mnd 17968  df-submnd 18013  df-grp 18162  df-minusg 18163  df-sbg 18164  df-subg 18333  df-cntz 18504  df-lsm 18818  df-cmn 18965  df-abl 18966  df-mgp 19298  df-ur 19310  df-ring 19357  df-oppr 19434  df-dvdsr 19452  df-unit 19453  df-invr 19483  df-dvr 19494  df-drng 19562  df-lmod 19694  df-lss 19762  df-lsp 19802  df-lvec 19933  df-oposet 36742  df-ol 36744  df-oml 36745  df-covers 36832  df-ats 36833  df-atl 36864  df-cvlat 36888  df-hlat 36917  df-llines 37064  df-lplanes 37065  df-lvols 37066  df-lines 37067  df-psubsp 37069  df-pmap 37070  df-padd 37362  df-lhyp 37554  df-laut 37555  df-ldil 37670  df-ltrn 37671  df-trl 37725  df-tendo 38321  df-edring 38323  df-disoa 38595  df-dvech 38645  df-dib 38705  df-dic 38739  df-dih 38795 This theorem is referenced by:  dihjatcc  38988
 Copyright terms: Public domain W3C validator