Metamath Proof Explorer

Theorem pmapojoinN

Description: For orthogonal elements, projective map of join equals projective sum. Compare pmapjoin where only one direction holds. (Contributed by NM, 11-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmapojoin.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapojoin.l ⊢ ≤ = ( le ‘ 𝐾 )
pmapojoin.j ⊢ ∨ = ( join ‘ 𝐾 )
pmapojoin.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
pmapojoin.o ⊢ ⊥ = ( oc ‘ 𝐾 )
pmapojoin.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion pmapojoinN ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 pmapojoin.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapojoin.l ⊢ ≤ = ( le ‘ 𝐾 )
3 pmapojoin.j ⊢ ∨ = ( join ‘ 𝐾 )
4 pmapojoin.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
5 pmapojoin.o ⊢ ⊥ = ( oc ‘ 𝐾 )
6 pmapojoin.p ⊢ + = ( +𝑃 ‘ 𝐾 )
7 eqid ⊢ ( ⊥𝑃 ‘ 𝐾 ) = ( ⊥𝑃 ‘ 𝐾 )
8 1 3 4 6 7 pmapj2N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ) ) )
9 8 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ) ) )
10 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → 𝐾 ∈ HL )
11 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → 𝑋 ∈ 𝐵 )
12 eqid ⊢ ( PSubCl ‘ 𝐾 ) = ( PSubCl ‘ 𝐾 )
13 1 4 12 pmapsubclN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ∈ ( PSubCl ‘ 𝐾 ) )
14 10 11 13 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( 𝑀 ‘ 𝑋 ) ∈ ( PSubCl ‘ 𝐾 ) )
15 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → 𝑌 ∈ 𝐵 )
16 1 4 12 pmapsubclN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑌 ) ∈ ( PSubCl ‘ 𝐾 ) )
17 10 15 16 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( 𝑀 ‘ 𝑌 ) ∈ ( PSubCl ‘ 𝐾 ) )
18 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
19 18 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP )
20 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
21 1 5 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
22 19 20 21 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
23 1 2 4 pmaple ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ↔ ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ ( ⊥ ‘ 𝑌 ) ) ) )
24 22 23 syld3an3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ↔ ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ ( ⊥ ‘ 𝑌 ) ) ) )
25 24 biimpa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ ( ⊥ ‘ 𝑌 ) ) )
26 1 5 4 7 polpmapN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑌 ) ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑌 ) ) )
27 10 15 26 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑌 ) ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑌 ) ) )
28 25 27 sseqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( 𝑀 ‘ 𝑋 ) ⊆ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑌 ) ) )
29 6 7 12 osumclN ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑀 ‘ 𝑋 ) ∈ ( PSubCl ‘ 𝐾 ) ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( PSubCl ‘ 𝐾 ) ) ∧ ( 𝑀 ‘ 𝑋 ) ⊆ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑌 ) ) ) → ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ∈ ( PSubCl ‘ 𝐾 ) )
30 10 14 17 28 29 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ∈ ( PSubCl ‘ 𝐾 ) )
31 7 12 psubcli2N ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ∈ ( PSubCl ‘ 𝐾 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) )
32 10 30 31 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) )
33 9 32 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) )