Theorem dihmeetlem20N 39034

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.)

Hypotheses

Ref	Expression
dihmeetlem14.b	⊢ 𝐵 = (Base‘𝐾)
dihmeetlem14.l	⊢ ≤ = (le‘𝐾)
dihmeetlem14.h	⊢ 𝐻 = (LHyp‘𝐾)
dihmeetlem14.j	⊢ ∨ = (join‘𝐾)
dihmeetlem14.m	⊢ ∧ = (meet‘𝐾)
dihmeetlem14.a	⊢ 𝐴 = (Atoms‘𝐾)
dihmeetlem14.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihmeetlem14.s	⊢ ⊕ = (LSSum‘𝑈)
dihmeetlem14.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)

Assertion

Ref	Expression
dihmeetlem20N	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))

Proof of Theorem dihmeetlem20N

Dummy variables 𝑟 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 1138	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp2 1139	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊))
3		simp3ll 1246	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → 𝑌 ∈ 𝐵)
4		simp3r 1204	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝑋 ∧ 𝑌) ≤ 𝑊)
5		dihmeetlem14.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
6		dihmeetlem14.l	. . . 4 ⊢ ≤ = (le‘𝐾)
7		dihmeetlem14.j	. . . 4 ⊢ ∨ = (join‘𝐾)
8		dihmeetlem14.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
9		dihmeetlem14.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
10		dihmeetlem14.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
11	5, 6, 7, 8, 9, 10	lhpmcvr6N 37736	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋))
12	1, 2, 3, 4, 11	syl112anc 1376	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋))
13		simp3l 1203	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊))
14		simp2l 1201	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → 𝑋 ∈ 𝐵)
15		simp1l 1199	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → 𝐾 ∈ HL)
16	15	hllatd 37072	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → 𝐾 ∈ Lat)
17	5, 8	latmcom 17941	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌 ∧ 𝑋) = (𝑋 ∧ 𝑌))
18	16, 3, 14, 17	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝑌 ∧ 𝑋) = (𝑋 ∧ 𝑌))
19	18, 4	eqbrtrd 5065	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝑌 ∧ 𝑋) ≤ 𝑊)
20	5, 6, 7, 8, 9, 10	lhpmcvr6N 37736	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ (𝑌 ∧ 𝑋) ≤ 𝑊)) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))
21	1, 13, 14, 19, 20	syl112anc 1376	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))
22		reeanv 3272	. . 3 ⊢ (∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)) ↔ (∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)))
23		simp11 1205	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
24		simp12 1206	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊))
25	3	3ad2ant1 1135	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → 𝑌 ∈ 𝐵)
26		simp2l 1201	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → 𝑞 ∈ 𝐴)
27		simp3l1 1280	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → ¬ 𝑞 ≤ 𝑊)
28	26, 27	jca 515	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
29		simp2r 1202	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → 𝑟 ∈ 𝐴)
30		simp3r1 1283	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → ¬ 𝑟 ≤ 𝑊)
31	29, 30	jca 515	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊))
32		simp3l3 1282	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → 𝑞 ≤ 𝑋)
33		simp3r3 1285	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → 𝑟 ≤ 𝑌)
34		simp13r 1291	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝑋 ∧ 𝑌) ≤ 𝑊)
35	32, 33, 34	3jca 1130	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝑞 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))
36		dihmeetlem14.u	. . . . . . 7 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
37		dihmeetlem14.s	. . . . . . 7 ⊢ ⊕ = (LSSum‘𝑈)
38		dihmeetlem14.i	. . . . . . 7 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
39	5, 6, 10, 7, 8, 9, 36, 37, 38	dihmeetlem19N 39033	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑞 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
40	23, 24, 25, 28, 31, 35, 39	syl33anc 1387	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
41	40	3exp 1121	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ((𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → (((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))))
42	41	rexlimdvv 3205	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))))
43	22, 42	syl5bir 246	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ((∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))))
44	12, 21, 43	mp2and 699	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110  ∃wrex 3055   ∩ cin 3856   class class class wbr 5043  ‘cfv 6369  (class class class)co 7202  Basecbs 16684  lecple 16774  joincjn 17790  meetcmee 17791  Latclat 17909  LSSumclsm 18995  Atomscatm 36971  HLchlt 37058  LHypclh 37692  DVecHcdvh 38786  DIsoHcdih 38936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-rep 5168  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512  ax-cnex 10768  ax-resscn 10769  ax-1cn 10770  ax-icn 10771  ax-addcl 10772  ax-addrcl 10773  ax-mulcl 10774  ax-mulrcl 10775  ax-mulcom 10776  ax-addass 10777  ax-mulass 10778  ax-distr 10779  ax-i2m1 10780  ax-1ne0 10781  ax-1rid 10782  ax-rnegex 10783  ax-rrecex 10784  ax-cnre 10785  ax-pre-lttri 10786  ax-pre-lttrn 10787  ax-pre-ltadd 10788  ax-pre-mulgt0 10789  ax-riotaBAD 36661

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-pss 3876  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-tp 4536  df-op 4538  df-uni 4810  df-int 4850  df-iun 4896  df-iin 4897  df-br 5044  df-opab 5106  df-mpt 5125  df-tr 5151  df-id 5444  df-eprel 5449  df-po 5457  df-so 5458  df-fr 5498  df-we 5500  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-pred 6149  df-ord 6205  df-on 6206  df-lim 6207  df-suc 6208  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-riota 7159  df-ov 7205  df-oprab 7206  df-mpo 7207  df-om 7634  df-1st 7750  df-2nd 7751  df-tpos 7957  df-undef 8004  df-wrecs 8036  df-recs 8097  df-rdg 8135  df-1o 8191  df-er 8380  df-map 8499  df-en 8616  df-dom 8617  df-sdom 8618  df-fin 8619  df-pnf 10852  df-mnf 10853  df-xr 10854  df-ltxr 10855  df-le 10856  df-sub 11047  df-neg 11048  df-nn 11814  df-2 11876  df-3 11877  df-4 11878  df-5 11879  df-6 11880  df-n0 12074  df-z 12160  df-uz 12422  df-fz 13079  df-struct 16686  df-ndx 16687  df-slot 16688  df-base 16690  df-sets 16691  df-ress 16692  df-plusg 16780  df-mulr 16781  df-sca 16783  df-vsca 16784  df-0g 16918  df-mre 17061  df-mrc 17062  df-acs 17064  df-proset 17774  df-poset 17792  df-plt 17808  df-lub 17824  df-glb 17825  df-join 17826  df-meet 17827  df-p0 17903  df-p1 17904  df-lat 17910  df-clat 17977  df-mgm 18086  df-sgrp 18135  df-mnd 18146  df-submnd 18191  df-grp 18340  df-minusg 18341  df-sbg 18342  df-subg 18512  df-cntz 18683  df-lsm 18997  df-cmn 19144  df-abl 19145  df-mgp 19477  df-ur 19489  df-ring 19536  df-oppr 19613  df-dvdsr 19631  df-unit 19632  df-invr 19662  df-dvr 19673  df-drng 19741  df-lmod 19873  df-lss 19941  df-lsp 19981  df-lvec 20112  df-oposet 36884  df-ol 36886  df-oml 36887  df-covers 36974  df-ats 36975  df-atl 37006  df-cvlat 37030  df-hlat 37059  df-llines 37206  df-lplanes 37207  df-lvols 37208  df-lines 37209  df-psubsp 37211  df-pmap 37212  df-padd 37504  df-lhyp 37696  df-laut 37697  df-ldil 37812  df-ltrn 37813  df-trl 37867  df-tendo 38463  df-edring 38465  df-disoa 38737  df-dvech 38787  df-dib 38847  df-dic 38881  df-dih 38937

This theorem is referenced by:  dihmeetALTN  39035