Metamath Proof Explorer

Theorem pmod1i

Description: The modular law holds in a projective subspace. (Contributed by NM, 10-Mar-2012)

Ref Expression
Hypotheses pmod.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pmod.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
pmod.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion pmod1i ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( 𝑋 ⊆ 𝑍 → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) = ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) )

Proof

Step Hyp Ref Expression
1 pmod.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 pmod.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3 pmod.p ⊢ + = ( +𝑃 ‘ 𝐾 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
6 4 5 1 2 3 pmodlem2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
7 6 3expa ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
8 inss1 ⊢ ( 𝑌 ∩ 𝑍 ) ⊆ 𝑌
9 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → 𝐾 ∈ HL )
10 simplr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → 𝑌 ⊆ 𝐴 )
11 simplr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → 𝑋 ⊆ 𝐴 )
12 1 3 paddss2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( ( 𝑌 ∩ 𝑍 ) ⊆ 𝑌 → ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ⊆ ( 𝑋 + 𝑌 ) ) )
13 9 10 11 12 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → ( ( 𝑌 ∩ 𝑍 ) ⊆ 𝑌 → ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ⊆ ( 𝑋 + 𝑌 ) ) )
14 8 13 mpi ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ⊆ ( 𝑋 + 𝑌 ) )
15 simpl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝐾 ∈ HL )
16 1 2 psubssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ∈ 𝑆 ) → 𝑍 ⊆ 𝐴 )
17 16 3ad2antr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝑍 ⊆ 𝐴 )
18 simpr2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝑌 ⊆ 𝐴 )
19 ssinss1 ⊢ ( 𝑌 ⊆ 𝐴 → ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 )
20 18 19 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 )
21 1 3 paddss1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ⊆ 𝐴 ∧ ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 ) → ( 𝑋 ⊆ 𝑍 → ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ⊆ ( 𝑍 + ( 𝑌 ∩ 𝑍 ) ) ) )
22 15 17 20 21 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( 𝑋 ⊆ 𝑍 → ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ⊆ ( 𝑍 + ( 𝑌 ∩ 𝑍 ) ) ) )
23 22 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ⊆ ( 𝑍 + ( 𝑌 ∩ 𝑍 ) ) )
24 simplr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → 𝑍 ∈ 𝑆 )
25 9 24 16 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → 𝑍 ⊆ 𝐴 )
26 inss2 ⊢ ( 𝑌 ∩ 𝑍 ) ⊆ 𝑍
27 1 3 paddss2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑌 ∩ 𝑍 ) ⊆ 𝑍 → ( 𝑍 + ( 𝑌 ∩ 𝑍 ) ) ⊆ ( 𝑍 + 𝑍 ) ) )
28 26 27 mpi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑍 + ( 𝑌 ∩ 𝑍 ) ) ⊆ ( 𝑍 + 𝑍 ) )
29 9 25 25 28 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → ( 𝑍 + ( 𝑌 ∩ 𝑍 ) ) ⊆ ( 𝑍 + 𝑍 ) )
30 2 3 paddidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ∈ 𝑆 ) → ( 𝑍 + 𝑍 ) = 𝑍 )
31 9 24 30 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → ( 𝑍 + 𝑍 ) = 𝑍 )
32 29 31 sseqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → ( 𝑍 + ( 𝑌 ∩ 𝑍 ) ) ⊆ 𝑍 )
33 23 32 sstrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ⊆ 𝑍 )
34 14 33 ssind ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) )
35 7 34 eqssd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) ∧ 𝑋 ⊆ 𝑍 ) → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) = ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
36 35 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( 𝑋 ⊆ 𝑍 → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) = ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) )