lvoli3

Description: Condition implying a 3-dim lattice volume. (Contributed by NM, 2-Aug-2012)

	Ref	Expression
Hypotheses	lvoli3.l	⊢ ≤ = ( le ‘ 𝐾 )
	lvoli3.j	⊢ ∨ = ( join ‘ 𝐾 )
	lvoli3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	lvoli3.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
	lvoli3.v	⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion	lvoli3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lvoli3.l	⊢ ≤ = ( le ‘ 𝐾 )
2		lvoli3.j	⊢ ∨ = ( join ‘ 𝐾 )
3		lvoli3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		lvoli3.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5		lvoli3.v	⊢ 𝑉 = ( LVols ‘ 𝐾 )
6		simpl2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑋 ∈ 𝑃 )
7		simpl3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑄 ∈ 𝐴 )
8		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ¬ 𝑄 ≤ 𝑋 )
9		eqidd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑄 ) )
10		breq2	⊢ ( 𝑦 = 𝑋 → ( 𝑟 ≤ 𝑦 ↔ 𝑟 ≤ 𝑋 ) )
11	10	notbid	⊢ ( 𝑦 = 𝑋 → ( ¬ 𝑟 ≤ 𝑦 ↔ ¬ 𝑟 ≤ 𝑋 ) )
12		oveq1	⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∨ 𝑟 ) = ( 𝑋 ∨ 𝑟 ) )
13	12	eqeq2d	⊢ ( 𝑦 = 𝑋 → ( ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ↔ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑟 ) ) )
14	11 13	anbi12d	⊢ ( 𝑦 = 𝑋 → ( ( ¬ 𝑟 ≤ 𝑦 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ) ↔ ( ¬ 𝑟 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑟 ) ) ) )
15		breq1	⊢ ( 𝑟 = 𝑄 → ( 𝑟 ≤ 𝑋 ↔ 𝑄 ≤ 𝑋 ) )
16	15	notbid	⊢ ( 𝑟 = 𝑄 → ( ¬ 𝑟 ≤ 𝑋 ↔ ¬ 𝑄 ≤ 𝑋 ) )
17		oveq2	⊢ ( 𝑟 = 𝑄 → ( 𝑋 ∨ 𝑟 ) = ( 𝑋 ∨ 𝑄 ) )
18	17	eqeq2d	⊢ ( 𝑟 = 𝑄 → ( ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑟 ) ↔ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑄 ) ) )
19	16 18	anbi12d	⊢ ( 𝑟 = 𝑄 → ( ( ¬ 𝑟 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑟 ) ) ↔ ( ¬ 𝑄 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑄 ) ) ) )
20	14 19	rspc2ev	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ ( ¬ 𝑄 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑄 ) ) ) → ∃ 𝑦 ∈ 𝑃 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ) )
21	6 7 8 9 20	syl112anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑃 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ) )
22		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝐾 ∈ HL )
23	22	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝐾 ∈ Lat )
24		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
25	24 4	lplnbase	⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
26	6 25	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
27	24 3	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
28	7 27	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
29	24 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
30	23 26 28 29	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( 𝑋 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
31	24 1 2 3 4 5	islvol3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑋 ∨ 𝑄 ) ∈ 𝑉 ↔ ∃ 𝑦 ∈ 𝑃 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ) ) )
32	22 30 31	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( ( 𝑋 ∨ 𝑄 ) ∈ 𝑉 ↔ ∃ 𝑦 ∈ 𝑃 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ) ) )
33	21 32	mpbird	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝑉 )

Metamath Proof Explorer

Theorem lvoli3

Proof