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

Theorem dihmeetlem1N 37904
Description: Isomorphism H of a conjunction. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dihglblem5a.b 𝐵 = (Base‘𝐾)
dihglblem5a.m = (meet‘𝐾)
dihglblem5a.h 𝐻 = (LHyp‘𝐾)
dihglblem5a.i 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dihglblem5a.l = (le‘𝐾)
dihglblem5a.j = (join‘𝐾)
dihglblem5a.a 𝐴 = (Atoms‘𝐾)
dihglblem5a.p 𝑃 = ((oc‘𝐾)‘𝑊)
dihglblem5a.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
dihglblem5a.r 𝑅 = ((trL‘𝐾)‘𝑊)
dihglblem5a.e 𝐸 = ((TEndo‘𝐾)‘𝑊)
dihglblem5a.g 𝐺 = (𝑇 (𝑃) = 𝑞)
dihglblem5a.o 0 = (𝑇 ↦ ( I ↾ 𝐵))
Assertion
Ref Expression
dihmeetlem1N (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝐼‘(𝑋 𝑌)) = ((𝐼𝑋) ∩ (𝐼𝑌)))
Distinct variable groups:   ,𝑞   ,𝑞,   𝐴,,𝑞   𝐵,,𝑞   ,𝐻,𝑞   𝐼,𝑞   ,𝐾,𝑞   𝑃,   𝑇,   ,𝑊,𝑞   𝑋,𝑞   𝑌,𝑞
Allowed substitution hints:   𝑃(𝑞)   𝑅(,𝑞)   𝑇(𝑞)   𝐸(,𝑞)   𝐺(,𝑞)   𝐼()   (,𝑞)   ()   𝑋()   𝑌()   0 (,𝑞)

Proof of Theorem dihmeetlem1N
Dummy variables 𝑓 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1l 1178 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → 𝐾 ∈ HL)
21hllatd 35978 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → 𝐾 ∈ Lat)
3 simp2l 1180 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → 𝑋𝐵)
4 simp3l 1182 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → 𝑌𝐵)
5 dihglblem5a.b . . . . . 6 𝐵 = (Base‘𝐾)
6 dihglblem5a.l . . . . . 6 = (le‘𝐾)
7 dihglblem5a.m . . . . . 6 = (meet‘𝐾)
85, 6, 7latmle1 17557 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑋)
92, 3, 4, 8syl3anc 1352 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝑋 𝑌) 𝑋)
10 simp1 1117 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
115, 7latmcl 17533 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
122, 3, 4, 11syl3anc 1352 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝑋 𝑌) ∈ 𝐵)
13 dihglblem5a.h . . . . . 6 𝐻 = (LHyp‘𝐾)
14 dihglblem5a.i . . . . . 6 𝐼 = ((DIsoH‘𝐾)‘𝑊)
155, 6, 13, 14dihord 37878 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 𝑌) ∈ 𝐵𝑋𝐵) → ((𝐼‘(𝑋 𝑌)) ⊆ (𝐼𝑋) ↔ (𝑋 𝑌) 𝑋))
1610, 12, 3, 15syl3anc 1352 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → ((𝐼‘(𝑋 𝑌)) ⊆ (𝐼𝑋) ↔ (𝑋 𝑌) 𝑋))
179, 16mpbird 249 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝐼‘(𝑋 𝑌)) ⊆ (𝐼𝑋))
185, 6, 7latmle2 17558 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑌)
192, 3, 4, 18syl3anc 1352 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝑋 𝑌) 𝑌)
205, 6, 13, 14dihord 37878 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 𝑌) ∈ 𝐵𝑌𝐵) → ((𝐼‘(𝑋 𝑌)) ⊆ (𝐼𝑌) ↔ (𝑋 𝑌) 𝑌))
2110, 12, 4, 20syl3anc 1352 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → ((𝐼‘(𝑋 𝑌)) ⊆ (𝐼𝑌) ↔ (𝑋 𝑌) 𝑌))
2219, 21mpbird 249 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝐼‘(𝑋 𝑌)) ⊆ (𝐼𝑌))
2317, 22ssind 4091 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝐼‘(𝑋 𝑌)) ⊆ ((𝐼𝑋) ∩ (𝐼𝑌)))
2413, 14dihvalrel 37893 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → Rel (𝐼𝑋))
25 relin1 5532 . . . . 5 (Rel (𝐼𝑋) → Rel ((𝐼𝑋) ∩ (𝐼𝑌)))
2624, 25syl 17 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → Rel ((𝐼𝑋) ∩ (𝐼𝑌)))
27263ad2ant1 1114 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → Rel ((𝐼𝑋) ∩ (𝐼𝑌)))
28 elin 4052 . . . 4 (⟨𝑓, 𝑠⟩ ∈ ((𝐼𝑋) ∩ (𝐼𝑌)) ↔ (⟨𝑓, 𝑠⟩ ∈ (𝐼𝑋) ∧ ⟨𝑓, 𝑠⟩ ∈ (𝐼𝑌)))
29 dihglblem5a.j . . . . . . 7 = (join‘𝐾)
30 dihglblem5a.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
315, 6, 29, 7, 30, 13lhpmcvr2 36638 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊)) → ∃𝑞𝐴𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))
32313adant3 1113 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → ∃𝑞𝐴𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))
33 simpl1 1172 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
34 simpl2 1173 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → (𝑋𝐵 ∧ ¬ 𝑋 𝑊))
35 simprl 759 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → 𝑞𝐴)
36 simprrl 769 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → ¬ 𝑞 𝑊)
3735, 36jca 504 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → (𝑞𝐴 ∧ ¬ 𝑞 𝑊))
38 simprrr 770 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → (𝑞 (𝑋 𝑊)) = 𝑋)
39 dihglblem5a.p . . . . . . . . 9 𝑃 = ((oc‘𝐾)‘𝑊)
40 dihglblem5a.t . . . . . . . . 9 𝑇 = ((LTrn‘𝐾)‘𝑊)
41 dihglblem5a.r . . . . . . . . 9 𝑅 = ((trL‘𝐾)‘𝑊)
42 dihglblem5a.e . . . . . . . . 9 𝐸 = ((TEndo‘𝐾)‘𝑊)
43 dihglblem5a.g . . . . . . . . 9 𝐺 = (𝑇 (𝑃) = 𝑞)
44 vex 3413 . . . . . . . . 9 𝑓 ∈ V
45 vex 3413 . . . . . . . . 9 𝑠 ∈ V
465, 6, 29, 7, 30, 13, 39, 40, 41, 42, 14, 43, 44, 45dihopelvalc 37863 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑞𝐴 ∧ ¬ 𝑞 𝑊) ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼𝑋) ↔ ((𝑓𝑇𝑠𝐸) ∧ (𝑅‘(𝑓(𝑠𝐺))) 𝑋)))
4733, 34, 37, 38, 46syl112anc 1355 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼𝑋) ↔ ((𝑓𝑇𝑠𝐸) ∧ (𝑅‘(𝑓(𝑠𝐺))) 𝑋)))
48 simpr 477 . . . . . . 7 (((𝑓𝑇𝑠𝐸) ∧ (𝑅‘(𝑓(𝑠𝐺))) 𝑋) → (𝑅‘(𝑓(𝑠𝐺))) 𝑋)
4947, 48syl6bi 245 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼𝑋) → (𝑅‘(𝑓(𝑠𝐺))) 𝑋))
50 simpl3 1174 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → (𝑌𝐵𝑌 𝑊))
51 dihglblem5a.o . . . . . . . . 9 0 = (𝑇 ↦ ( I ↾ 𝐵))
525, 6, 13, 40, 41, 51, 14dihopelvalbN 37852 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑌𝐵𝑌 𝑊)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼𝑌) ↔ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 )))
5333, 50, 52syl2anc 576 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼𝑌) ↔ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 )))
5453biimpd 221 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼𝑌) → ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 )))
55 simprll 767 . . . . . . . . . 10 (((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 )) → 𝑓𝑇)
56553ad2ant3 1116 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝑓𝑇)
57 simp3rr 1228 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝑠 = 0 )
5857fveq1d 6499 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑠𝐺) = ( 0𝐺))
59 simp11 1184 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
606, 30, 13, 39lhpocnel2 36633 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
6159, 60syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
62 simp2l 1180 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝑞𝐴)
63 simp2rl 1223 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → ¬ 𝑞 𝑊)
646, 30, 13, 40, 43ltrniotacl 37193 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑞𝐴 ∧ ¬ 𝑞 𝑊)) → 𝐺𝑇)
6559, 61, 62, 63, 64syl112anc 1355 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝐺𝑇)
6651, 5tendo02 37401 . . . . . . . . . . . . . . . . . 18 (𝐺𝑇 → ( 0𝐺) = ( I ↾ 𝐵))
6765, 66syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → ( 0𝐺) = ( I ↾ 𝐵))
6858, 67eqtrd 2809 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑠𝐺) = ( I ↾ 𝐵))
6968cnveqd 5593 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑠𝐺) = ( I ↾ 𝐵))
70 cnvresid 6264 . . . . . . . . . . . . . . 15 ( I ↾ 𝐵) = ( I ↾ 𝐵)
7169, 70syl6eq 2825 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑠𝐺) = ( I ↾ 𝐵))
7271coeq2d 5580 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑓(𝑠𝐺)) = (𝑓 ∘ ( I ↾ 𝐵)))
735, 13, 40ltrn1o 36738 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑓𝑇) → 𝑓:𝐵1-1-onto𝐵)
7459, 56, 73syl2anc 576 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝑓:𝐵1-1-onto𝐵)
75 f1of 6442 . . . . . . . . . . . . . 14 (𝑓:𝐵1-1-onto𝐵𝑓:𝐵𝐵)
76 fcoi1 6379 . . . . . . . . . . . . . 14 (𝑓:𝐵𝐵 → (𝑓 ∘ ( I ↾ 𝐵)) = 𝑓)
7774, 75, 763syl 18 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑓 ∘ ( I ↾ 𝐵)) = 𝑓)
7872, 77eqtrd 2809 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑓(𝑠𝐺)) = 𝑓)
7978fveq2d 6501 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑅‘(𝑓(𝑠𝐺))) = (𝑅𝑓))
80 simp3l 1182 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑅‘(𝑓(𝑠𝐺))) 𝑋)
8179, 80eqbrtrrd 4950 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑅𝑓) 𝑋)
82 simprlr 768 . . . . . . . . . . 11 (((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 )) → (𝑅𝑓) 𝑌)
83823ad2ant3 1116 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑅𝑓) 𝑌)
84 simp11l 1265 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝐾 ∈ HL)
8584hllatd 35978 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝐾 ∈ Lat)
865, 13, 40, 41trlcl 36778 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑓𝑇) → (𝑅𝑓) ∈ 𝐵)
8759, 56, 86syl2anc 576 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑅𝑓) ∈ 𝐵)
88 simp12l 1267 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝑋𝐵)
89 simp13l 1269 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝑌𝐵)
905, 6, 7latlem12 17559 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ ((𝑅𝑓) ∈ 𝐵𝑋𝐵𝑌𝐵)) → (((𝑅𝑓) 𝑋 ∧ (𝑅𝑓) 𝑌) ↔ (𝑅𝑓) (𝑋 𝑌)))
9185, 87, 88, 89, 90syl13anc 1353 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (((𝑅𝑓) 𝑋 ∧ (𝑅𝑓) 𝑌) ↔ (𝑅𝑓) (𝑋 𝑌)))
9281, 83, 91mpbi2and 700 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑅𝑓) (𝑋 𝑌))
9356, 92jca 504 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑌)))
9485, 88, 89, 11syl3anc 1352 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑋 𝑌) ∈ 𝐵)
95 simp11r 1266 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝑊𝐻)
965, 13lhpbase 36612 . . . . . . . . . . 11 (𝑊𝐻𝑊𝐵)
9795, 96syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝑊𝐵)
9885, 88, 89, 18syl3anc 1352 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑋 𝑌) 𝑌)
99 simp13r 1270 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → 𝑌 𝑊)
1005, 6, 85, 94, 89, 97, 98, 99lattrd 17539 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (𝑋 𝑌) 𝑊)
1015, 6, 13, 40, 41, 51, 14dihopelvalbN 37852 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑋 𝑌) ∈ 𝐵 ∧ (𝑋 𝑌) 𝑊)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 𝑌)) ↔ ((𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑌)) ∧ 𝑠 = 0 )))
10259, 94, 100, 101syl12anc 825 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 𝑌)) ↔ ((𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑌)) ∧ 𝑠 = 0 )))
10393, 57, 102mpbir2and 701 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 ))) → ⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 𝑌)))
1041033expia 1102 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → (((𝑅‘(𝑓(𝑠𝐺))) 𝑋 ∧ ((𝑓𝑇 ∧ (𝑅𝑓) 𝑌) ∧ 𝑠 = 0 )) → ⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 𝑌))))
10549, 54, 104syl2and 599 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (𝑞𝐴 ∧ (¬ 𝑞 𝑊 ∧ (𝑞 (𝑋 𝑊)) = 𝑋))) → ((⟨𝑓, 𝑠⟩ ∈ (𝐼𝑋) ∧ ⟨𝑓, 𝑠⟩ ∈ (𝐼𝑌)) → ⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 𝑌))))
10632, 105rexlimddv 3231 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → ((⟨𝑓, 𝑠⟩ ∈ (𝐼𝑋) ∧ ⟨𝑓, 𝑠⟩ ∈ (𝐼𝑌)) → ⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 𝑌))))
10728, 106syl5bi 234 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (⟨𝑓, 𝑠⟩ ∈ ((𝐼𝑋) ∩ (𝐼𝑌)) → ⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝑋 𝑌))))
10827, 107relssdv 5508 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → ((𝐼𝑋) ∩ (𝐼𝑌)) ⊆ (𝐼‘(𝑋 𝑌)))
10923, 108eqssd 3870 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝐼‘(𝑋 𝑌)) = ((𝐼𝑋) ∩ (𝐼𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1069   = wceq 1508  wcel 2051  wrex 3084  cin 3823  wss 3824  cop 4442   class class class wbr 4926  cmpt 5005   I cid 5308  ccnv 5403  cres 5406  ccom 5408  Rel wrel 5409  wf 6182  1-1-ontowf1o 6185  cfv 6186  crio 6935  (class class class)co 6975  Basecbs 16338  lecple 16427  occoc 16428  joincjn 17425  meetcmee 17426  Latclat 17526  Atomscatm 35877  HLchlt 35964  LHypclh 36598  LTrncltrn 36715  trLctrl 36772  TEndoctendo 37366  DIsoHcdih 37842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-cnex 10390  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411  ax-riotaBAD 35567
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-int 4747  df-iun 4791  df-iin 4792  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-om 7396  df-1st 7500  df-2nd 7501  df-tpos 7694  df-undef 7741  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-1o 7904  df-oadd 7908  df-er 8088  df-map 8207  df-en 8306  df-dom 8307  df-sdom 8308  df-fin 8309  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-nn 11439  df-2 11502  df-3 11503  df-4 11504  df-5 11505  df-6 11506  df-n0 11707  df-z 11793  df-uz 12058  df-fz 12708  df-struct 16340  df-ndx 16341  df-slot 16342  df-base 16344  df-sets 16345  df-ress 16346  df-plusg 16433  df-mulr 16434  df-sca 16436  df-vsca 16437  df-0g 16570  df-proset 17409  df-poset 17427  df-plt 17439  df-lub 17455  df-glb 17456  df-join 17457  df-meet 17458  df-p0 17520  df-p1 17521  df-lat 17527  df-clat 17589  df-mgm 17723  df-sgrp 17765  df-mnd 17776  df-submnd 17817  df-grp 17907  df-minusg 17908  df-sbg 17909  df-subg 18073  df-cntz 18231  df-lsm 18535  df-cmn 18681  df-abl 18682  df-mgp 18976  df-ur 18988  df-ring 19035  df-oppr 19109  df-dvdsr 19127  df-unit 19128  df-invr 19158  df-dvr 19169  df-drng 19240  df-lmod 19371  df-lss 19439  df-lsp 19479  df-lvec 19610  df-oposet 35790  df-ol 35792  df-oml 35793  df-covers 35880  df-ats 35881  df-atl 35912  df-cvlat 35936  df-hlat 35965  df-llines 36112  df-lplanes 36113  df-lvols 36114  df-lines 36115  df-psubsp 36117  df-pmap 36118  df-padd 36410  df-lhyp 36602  df-laut 36603  df-ldil 36718  df-ltrn 36719  df-trl 36773  df-tendo 37369  df-edring 37371  df-disoa 37643  df-dvech 37693  df-dib 37753  df-dic 37787  df-dih 37843
This theorem is referenced by:  dihmeetbN  37917
  Copyright terms: Public domain W3C validator