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	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pmapojoin.j	$⊢ \underset{˙}{\lor} = join (K)$
	pmapojoin.m	$⊢ M = pmap (K)$
	pmapojoin.o	$⊢ \underset{˙}{⊥} = oc (K)$
	pmapojoin.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	pmapojoinN	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{\leq} \underset{˙}{⊥} (Y)) \to M (X \underset{˙}{\lor} Y) = M (X) \underset{˙}{+} M (Y)$

Proof

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

Metamath Proof Explorer

Theorem pmapojoinN

Proof