Theorem 2llnjN 39676

Description: The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012.) (New usage is discouraged.)

Hypotheses

Ref	Expression
2llnj.l	⊢ ≤ = (le‘𝐾)
2llnj.j	⊢ ∨ = (join‘𝐾)
2llnj.n	⊢ 𝑁 = (LLines‘𝐾)
2llnj.p	⊢ 𝑃 = (LPlanes‘𝐾)

Assertion

Ref	Expression
2llnjN	⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → (𝑋 ∨ 𝑌) = 𝑊)

Proof of Theorem 2llnjN

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

Step	Hyp	Ref	Expression
1		eqid 2733	. . . . . . . 8 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		2llnj.j	. . . . . . . 8 ⊢ ∨ = (join‘𝐾)
3		eqid 2733	. . . . . . . 8 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
4		2llnj.n	. . . . . . . 8 ⊢ 𝑁 = (LLines‘𝐾)
5	1, 2, 3, 4	islln2 39620	. . . . . . 7 ⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝑁 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟)))))
6		simpr 484	. . . . . . 7 ⊢ ((𝑋 ∈ (Base‘𝐾) ∧ ∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) → ∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟)))
7	5, 6	biimtrdi 253	. . . . . 6 ⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝑁 → ∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))))
8	1, 2, 3, 4	islln2 39620	. . . . . . 7 ⊢ (𝐾 ∈ HL → (𝑌 ∈ 𝑁 ↔ (𝑌 ∈ (Base‘𝐾) ∧ ∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))))
9		simpr 484	. . . . . . 7 ⊢ ((𝑌 ∈ (Base‘𝐾) ∧ ∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡))) → ∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))
10	8, 9	biimtrdi 253	. . . . . 6 ⊢ (𝐾 ∈ HL → (𝑌 ∈ 𝑁 → ∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡))))
11	7, 10	anim12d 609	. . . . 5 ⊢ (𝐾 ∈ HL → ((𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) → (∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟)) ∧ ∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))))
12	11	imp 406	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟)) ∧ ∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡))))
13	12	3adantr3 1172	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃)) → (∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟)) ∧ ∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡))))
14	13	3adant3 1132	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → (∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟)) ∧ ∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡))))
15		simp2rr 1244	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → 𝑋 = (𝑞 ∨ 𝑟))
16		simp3rr 1248	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → 𝑌 = (𝑠 ∨ 𝑡))
17	15, 16	oveq12d 7373	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → (𝑋 ∨ 𝑌) = ((𝑞 ∨ 𝑟) ∨ (𝑠 ∨ 𝑡)))
18		simp13 1206	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌))
19		breq1 5098	. . . . . . . . . . . . . . 15 ⊢ (𝑋 = (𝑞 ∨ 𝑟) → (𝑋 ≤ 𝑊 ↔ (𝑞 ∨ 𝑟) ≤ 𝑊))
20		neeq1 2992	. . . . . . . . . . . . . . 15 ⊢ (𝑋 = (𝑞 ∨ 𝑟) → (𝑋 ≠ 𝑌 ↔ (𝑞 ∨ 𝑟) ≠ 𝑌))
21	19, 20	3anbi13d 1440	. . . . . . . . . . . . . 14 ⊢ (𝑋 = (𝑞 ∨ 𝑟) → ((𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌) ↔ ((𝑞 ∨ 𝑟) ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ (𝑞 ∨ 𝑟) ≠ 𝑌)))
22		breq1 5098	. . . . . . . . . . . . . . 15 ⊢ (𝑌 = (𝑠 ∨ 𝑡) → (𝑌 ≤ 𝑊 ↔ (𝑠 ∨ 𝑡) ≤ 𝑊))
23		neeq2 2993	. . . . . . . . . . . . . . 15 ⊢ (𝑌 = (𝑠 ∨ 𝑡) → ((𝑞 ∨ 𝑟) ≠ 𝑌 ↔ (𝑞 ∨ 𝑟) ≠ (𝑠 ∨ 𝑡)))
24	22, 23	3anbi23d 1441	. . . . . . . . . . . . . 14 ⊢ (𝑌 = (𝑠 ∨ 𝑡) → (((𝑞 ∨ 𝑟) ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ (𝑞 ∨ 𝑟) ≠ 𝑌) ↔ ((𝑞 ∨ 𝑟) ≤ 𝑊 ∧ (𝑠 ∨ 𝑡) ≤ 𝑊 ∧ (𝑞 ∨ 𝑟) ≠ (𝑠 ∨ 𝑡))))
25	21, 24	sylan9bb 509	. . . . . . . . . . . . 13 ⊢ ((𝑋 = (𝑞 ∨ 𝑟) ∧ 𝑌 = (𝑠 ∨ 𝑡)) → ((𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌) ↔ ((𝑞 ∨ 𝑟) ≤ 𝑊 ∧ (𝑠 ∨ 𝑡) ≤ 𝑊 ∧ (𝑞 ∨ 𝑟) ≠ (𝑠 ∨ 𝑡))))
26	15, 16, 25	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → ((𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌) ↔ ((𝑞 ∨ 𝑟) ≤ 𝑊 ∧ (𝑠 ∨ 𝑡) ≤ 𝑊 ∧ (𝑞 ∨ 𝑟) ≠ (𝑠 ∨ 𝑡))))
27	18, 26	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → ((𝑞 ∨ 𝑟) ≤ 𝑊 ∧ (𝑠 ∨ 𝑡) ≤ 𝑊 ∧ (𝑞 ∨ 𝑟) ≠ (𝑠 ∨ 𝑡)))
28		simp11 1204	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → 𝐾 ∈ HL)
29		simp123 1308	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → 𝑊 ∈ 𝑃)
30		simp2ll 1241	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → 𝑞 ∈ (Atoms‘𝐾))
31		simp2lr 1242	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → 𝑟 ∈ (Atoms‘𝐾))
32		simp2rl 1243	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → 𝑞 ≠ 𝑟)
33		simp3ll 1245	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → 𝑠 ∈ (Atoms‘𝐾))
34		simp3lr 1246	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → 𝑡 ∈ (Atoms‘𝐾))
35		simp3rl 1247	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → 𝑠 ≠ 𝑡)
36		2llnj.l	. . . . . . . . . . . . . 14 ⊢ ≤ = (le‘𝐾)
37		2llnj.p	. . . . . . . . . . . . . 14 ⊢ 𝑃 = (LPlanes‘𝐾)
38	36, 2, 3, 4, 37	2llnjaN 39675	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾) ∧ 𝑞 ≠ 𝑟) ∧ (𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾) ∧ 𝑠 ≠ 𝑡)) ∧ ((𝑞 ∨ 𝑟) ≤ 𝑊 ∧ (𝑠 ∨ 𝑡) ≤ 𝑊 ∧ (𝑞 ∨ 𝑟) ≠ (𝑠 ∨ 𝑡))) → ((𝑞 ∨ 𝑟) ∨ (𝑠 ∨ 𝑡)) = 𝑊)
39	38	ex 412	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾) ∧ 𝑞 ≠ 𝑟) ∧ (𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾) ∧ 𝑠 ≠ 𝑡)) → (((𝑞 ∨ 𝑟) ≤ 𝑊 ∧ (𝑠 ∨ 𝑡) ≤ 𝑊 ∧ (𝑞 ∨ 𝑟) ≠ (𝑠 ∨ 𝑡)) → ((𝑞 ∨ 𝑟) ∨ (𝑠 ∨ 𝑡)) = 𝑊))
40	28, 29, 30, 31, 32, 33, 34, 35, 39	syl233anc 1401	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → (((𝑞 ∨ 𝑟) ≤ 𝑊 ∧ (𝑠 ∨ 𝑡) ≤ 𝑊 ∧ (𝑞 ∨ 𝑟) ≠ (𝑠 ∨ 𝑡)) → ((𝑞 ∨ 𝑟) ∨ (𝑠 ∨ 𝑡)) = 𝑊))
41	27, 40	mpd 15	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → ((𝑞 ∨ 𝑟) ∨ (𝑠 ∨ 𝑡)) = 𝑊)
42	17, 41	eqtrd 2768	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) ∧ ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)))) → (𝑋 ∨ 𝑌) = 𝑊)
43	42	3exp 1119	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → (((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) → (((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡))) → (𝑋 ∨ 𝑌) = 𝑊)))
44	43	3impib 1116	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) → (((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) ∧ (𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡))) → (𝑋 ∨ 𝑌) = 𝑊))
45	44	expd 415	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) → ((𝑠 ∈ (Atoms‘𝐾) ∧ 𝑡 ∈ (Atoms‘𝐾)) → ((𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)) → (𝑋 ∨ 𝑌) = 𝑊)))
46	45	rexlimdvv 3190	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟))) → (∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)) → (𝑋 ∨ 𝑌) = 𝑊))
47	46	3exp 1119	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) → ((𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟)) → (∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)) → (𝑋 ∨ 𝑌) = 𝑊))))
48	47	rexlimdvv 3190	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → (∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟)) → (∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡)) → (𝑋 ∨ 𝑌) = 𝑊)))
49	48	impd 410	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → ((∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑋 = (𝑞 ∨ 𝑟)) ∧ ∃𝑠 ∈ (Atoms‘𝐾)∃𝑡 ∈ (Atoms‘𝐾)(𝑠 ≠ 𝑡 ∧ 𝑌 = (𝑠 ∨ 𝑡))) → (𝑋 ∨ 𝑌) = 𝑊))
50	14, 49	mpd 15	1 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → (𝑋 ∨ 𝑌) = 𝑊)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ≠ wne 2930  ∃wrex 3058   class class class wbr 5095  ‘cfv 6489  (class class class)co 7355  Basecbs 17130  lecple 17178  joincjn 18227  Atomscatm 39372  HLchlt 39459  LLinesclln 39600  LPlanesclpl 39601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-proset 18210  df-poset 18229  df-plt 18244  df-lub 18260  df-glb 18261  df-join 18262  df-meet 18263  df-p0 18339  df-lat 18348  df-clat 18415  df-oposet 39285  df-ol 39287  df-oml 39288  df-covers 39375  df-ats 39376  df-atl 39407  df-cvlat 39431  df-hlat 39460  df-llines 39607  df-lplanes 39608

This theorem is referenced by:  2llnm2N  39677