paddcom

Description: Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012)

	Ref	Expression
Hypotheses	padd0.a	$⊢ A = Atoms (K)$
	padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	paddcom	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Proof

Step	Hyp	Ref	Expression
1		padd0.a	$⊢ A = Atoms (K)$
2		padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		uncom	$⊢ X \cup Y = Y \cup X$
4	3	a1i	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to X \cup Y = Y \cup X$
5		simpl1	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to K \in Lat$
6		simpl2	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to X \subseteq A$
7		simprl	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to q \in X$
8	6 7	sseldd	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to q \in A$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 1	atbase	$⊢ q \in A \to q \in {Base}_{K}$
11	8 10	syl	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to q \in {Base}_{K}$
12		simpl3	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to Y \subseteq A$
13		simprr	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to r \in Y$
14	12 13	sseldd	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to r \in A$
15	9 1	atbase	$⊢ r \in A \to r \in {Base}_{K}$
16	14 15	syl	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to r \in {Base}_{K}$
17		eqid	$⊢ join (K) = join (K)$
18	9 17	latjcom	$⊢ (K \in Lat \land q \in {Base}_{K} \land r \in {Base}_{K}) \to q join (K) r = r join (K) q$
19	5 11 16 18	syl3anc	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to q join (K) r = r join (K) q$
20	19	breq2d	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (q \in X \land r \in Y)) \to (p \leq_{K} (q join (K) r) \leftrightarrow p \leq_{K} (r join (K) q))$
21	20	2rexbidva	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to (\exists q \in X \exists r \in Y p \leq_{K} (q join (K) r) \leftrightarrow \exists q \in X \exists r \in Y p \leq_{K} (r join (K) q))$
22		rexcom	$⊢ \exists q \in X \exists r \in Y p \leq_{K} (r join (K) q) \leftrightarrow \exists r \in Y \exists q \in X p \leq_{K} (r join (K) q)$
23	21 22	bitrdi	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to (\exists q \in X \exists r \in Y p \leq_{K} (q join (K) r) \leftrightarrow \exists r \in Y \exists q \in X p \leq_{K} (r join (K) q))$
24	23	rabbidv	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to \{p \in A \| \exists q \in X \exists r \in Y p \leq_{K} (q join (K) r)\} = \{p \in A \| \exists r \in Y \exists q \in X p \leq_{K} (r join (K) q)\}$
25	4 24	uneq12d	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to (X \cup Y) \cup \{p \in A \| \exists q \in X \exists r \in Y p \leq_{K} (q join (K) r)\} = (Y \cup X) \cup \{p \in A \| \exists r \in Y \exists q \in X p \leq_{K} (r join (K) q)\}$
26		eqid	$⊢ \leq_{K} = \leq_{K}$
27	26 17 1 2	paddval	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y = (X \cup Y) \cup \{p \in A \| \exists q \in X \exists r \in Y p \leq_{K} (q join (K) r)\}$
28	26 17 1 2	paddval	$⊢ (K \in Lat \land Y \subseteq A \land X \subseteq A) \to Y \underset{˙}{+} X = (Y \cup X) \cup \{p \in A \| \exists r \in Y \exists q \in X p \leq_{K} (r join (K) q)\}$
29	28	3com23	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to Y \underset{˙}{+} X = (Y \cup X) \cup \{p \in A \| \exists r \in Y \exists q \in X p \leq_{K} (r join (K) q)\}$
30	25 27 29	3eqtr4d	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Metamath Proof Explorer

Theorem paddcom

Proof