This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmodN

Description: The modular law for projective subspaces. (Contributed by NM, 26-Mar-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pmod.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 pmod.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3 pmod.p ⊢ + = ( +𝑃 ‘ 𝐾 )
4 incom ⊢ ( 𝑋 ∩ ( ( 𝑋 ∩ 𝑍 ) + 𝑌 ) ) = ( ( ( 𝑋 ∩ 𝑍 ) + 𝑌 ) ∩ 𝑋 )
5 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
6 5 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝐾 ∈ Lat )
7 simpr2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑌 ⊆ 𝐴 )
8 inss2 ⊢ ( 𝑋 ∩ 𝑍 ) ⊆ 𝑍
9 simpr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑍 ⊆ 𝐴 )
10 8 9 sstrid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 ∩ 𝑍 ) ⊆ 𝐴 )
11 1 3 paddcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ⊆ 𝐴 ∧ ( 𝑋 ∩ 𝑍 ) ⊆ 𝐴 ) → ( 𝑌 + ( 𝑋 ∩ 𝑍 ) ) = ( ( 𝑋 ∩ 𝑍 ) + 𝑌 ) )
12 6 7 10 11 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑌 + ( 𝑋 ∩ 𝑍 ) ) = ( ( 𝑋 ∩ 𝑍 ) + 𝑌 ) )
13 12 ineq2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 ∩ ( 𝑌 + ( 𝑋 ∩ 𝑍 ) ) ) = ( 𝑋 ∩ ( ( 𝑋 ∩ 𝑍 ) + 𝑌 ) ) )
14 incom ⊢ ( 𝑋 ∩ 𝑌 ) = ( 𝑌 ∩ 𝑋 )
15 14 oveq2i ⊢ ( ( 𝑋 ∩ 𝑍 ) + ( 𝑋 ∩ 𝑌 ) ) = ( ( 𝑋 ∩ 𝑍 ) + ( 𝑌 ∩ 𝑋 ) )
16 inss2 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌
17 16 7 sstrid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 ∩ 𝑌 ) ⊆ 𝐴 )
18 1 3 paddcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∩ 𝑌 ) ⊆ 𝐴 ∧ ( 𝑋 ∩ 𝑍 ) ⊆ 𝐴 ) → ( ( 𝑋 ∩ 𝑌 ) + ( 𝑋 ∩ 𝑍 ) ) = ( ( 𝑋 ∩ 𝑍 ) + ( 𝑋 ∩ 𝑌 ) ) )
19 6 17 10 18 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 ∩ 𝑌 ) + ( 𝑋 ∩ 𝑍 ) ) = ( ( 𝑋 ∩ 𝑍 ) + ( 𝑋 ∩ 𝑌 ) ) )
20 simpr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑋 ∈ 𝑆 )
21 10 7 20 3jca ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 ∩ 𝑍 ) ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) )
22 inss1 ⊢ ( 𝑋 ∩ 𝑍 ) ⊆ 𝑋
23 1 2 3 pmod1i ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ∩ 𝑍 ) ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) ) → ( ( 𝑋 ∩ 𝑍 ) ⊆ 𝑋 → ( ( ( 𝑋 ∩ 𝑍 ) + 𝑌 ) ∩ 𝑋 ) = ( ( 𝑋 ∩ 𝑍 ) + ( 𝑌 ∩ 𝑋 ) ) ) )
24 22 23 mpi ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ∩ 𝑍 ) ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) ) → ( ( ( 𝑋 ∩ 𝑍 ) + 𝑌 ) ∩ 𝑋 ) = ( ( 𝑋 ∩ 𝑍 ) + ( 𝑌 ∩ 𝑋 ) ) )
25 21 24 syldan ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( ( 𝑋 ∩ 𝑍 ) + 𝑌 ) ∩ 𝑋 ) = ( ( 𝑋 ∩ 𝑍 ) + ( 𝑌 ∩ 𝑋 ) ) )
26 15 19 25 3eqtr4a ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 ∩ 𝑌 ) + ( 𝑋 ∩ 𝑍 ) ) = ( ( ( 𝑋 ∩ 𝑍 ) + 𝑌 ) ∩ 𝑋 ) )
27 4 13 26 3eqtr4a ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 ∩ ( 𝑌 + ( 𝑋 ∩ 𝑍 ) ) ) = ( ( 𝑋 ∩ 𝑌 ) + ( 𝑋 ∩ 𝑍 ) ) )