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 B = Base K
pmapojoin.l ˙ = K
pmapojoin.j ˙ = join K
pmapojoin.m M = pmap K
pmapojoin.o ˙ = oc K
pmapojoin.p + ˙ = + 𝑃 K
Assertion pmapojoinN K HL X B Y B X ˙ ˙ Y M X ˙ Y = M X + ˙ M Y

Proof

Step Hyp Ref Expression
1 pmapojoin.b B = Base K
2 pmapojoin.l ˙ = K
3 pmapojoin.j ˙ = join K
4 pmapojoin.m M = pmap K
5 pmapojoin.o ˙ = oc K
6 pmapojoin.p + ˙ = + 𝑃 K
7 eqid 𝑃 K = 𝑃 K
8 1 3 4 6 7 pmapj2N K HL X B Y B M X ˙ Y = 𝑃 K 𝑃 K M X + ˙ M Y
9 8 adantr K HL X B Y B X ˙ ˙ Y M X ˙ Y = 𝑃 K 𝑃 K M X + ˙ M Y
10 simpl1 K HL X B Y B X ˙ ˙ Y K HL
11 simpl2 K HL X B Y B X ˙ ˙ Y X B
12 eqid PSubCl K = PSubCl K
13 1 4 12 pmapsubclN K HL X B M X PSubCl K
14 10 11 13 syl2anc K HL X B Y B X ˙ ˙ Y M X PSubCl K
15 simpl3 K HL X B Y B X ˙ ˙ Y Y B
16 1 4 12 pmapsubclN K HL Y B M Y PSubCl K
17 10 15 16 syl2anc K HL X B Y B X ˙ ˙ Y M Y PSubCl K
18 hlop K HL K OP
19 18 3ad2ant1 K HL X B Y B K OP
20 simp3 K HL X B Y B Y B
21 1 5 opoccl K OP Y B ˙ Y B
22 19 20 21 syl2anc K HL X B Y B ˙ Y B
23 1 2 4 pmaple K HL X B ˙ Y B X ˙ ˙ Y M X M ˙ Y
24 22 23 syld3an3 K HL X B Y B X ˙ ˙ Y M X M ˙ Y
25 24 biimpa K HL X B Y B X ˙ ˙ Y M X M ˙ Y
26 1 5 4 7 polpmapN K HL Y B 𝑃 K M Y = M ˙ Y
27 10 15 26 syl2anc K HL X B Y B X ˙ ˙ Y 𝑃 K M Y = M ˙ Y
28 25 27 sseqtrrd K HL X B Y B X ˙ ˙ Y M X 𝑃 K M Y
29 6 7 12 osumclN K HL M X PSubCl K M Y PSubCl K M X 𝑃 K M Y M X + ˙ M Y PSubCl K
30 10 14 17 28 29 syl31anc K HL X B Y B X ˙ ˙ Y M X + ˙ M Y PSubCl K
31 7 12 psubcli2N K HL M X + ˙ M Y PSubCl K 𝑃 K 𝑃 K M X + ˙ M Y = M X + ˙ M Y
32 10 30 31 syl2anc K HL X B Y B X ˙ ˙ Y 𝑃 K 𝑃 K M X + ˙ M Y = M X + ˙ M Y
33 9 32 eqtrd K HL X B Y B X ˙ ˙ Y M X ˙ Y = M X + ˙ M Y