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 ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 ( 𝑌 ) ) → ( 𝑀 ‘ ( 𝑋 𝑌 ) ) = ( ( 𝑀𝑋 ) + ( 𝑀𝑌 ) ) )