elpaddn0

Description: Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012)

	Ref	Expression
Hypotheses	paddfval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	paddfval.j	$⊢ \underset{˙}{\lor} = join (K)$
	paddfval.a	$⊢ A = Atoms (K)$
	paddfval.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	elpaddn0	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in (X \underset{˙}{+} Y) \leftrightarrow (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$

Proof

Step	Hyp	Ref	Expression
1		paddfval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		paddfval.j	$⊢ \underset{˙}{\lor} = join (K)$
3		paddfval.a	$⊢ A = Atoms (K)$
4		paddfval.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5	1 2 3 4	elpadd	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to (S \in (X \underset{˙}{+} Y) \leftrightarrow ((S \in X \lor S \in Y) \lor (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))))$
6	5	adantr	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in (X \underset{˙}{+} Y) \leftrightarrow ((S \in X \lor S \in Y) \lor (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))))$
7		simpl2	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to X \subseteq A$
8	7	sseld	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in X \to S \in A)$
9		simpll1	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in X) \land r \in Y) \to K \in Lat$
10		ssel2	$⊢ (X \subseteq A \land S \in X) \to S \in A$
11	10	3ad2antl2	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in X) \to S \in A$
12	11	adantr	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in X) \land r \in Y) \to S \in A$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
15	12 14	syl	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in X) \land r \in Y) \to S \in {Base}_{K}$
16		simpl3	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in X) \to Y \subseteq A$
17	16	sselda	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in X) \land r \in Y) \to r \in A$
18	13 3	atbase	$⊢ r \in A \to r \in {Base}_{K}$
19	17 18	syl	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in X) \land r \in Y) \to r \in {Base}_{K}$
20	13 1 2	latlej1	$⊢ (K \in Lat \land S \in {Base}_{K} \land r \in {Base}_{K}) \to S \underset{˙}{\leq} (S \underset{˙}{\lor} r)$
21	9 15 19 20	syl3anc	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in X) \land r \in Y) \to S \underset{˙}{\leq} (S \underset{˙}{\lor} r)$
22	21	reximdva0	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in X) \land Y \neq \emptyset) \to \exists r \in Y S \underset{˙}{\leq} (S \underset{˙}{\lor} r)$
23	22	exp31	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to (S \in X \to (Y \neq \emptyset \to \exists r \in Y S \underset{˙}{\leq} (S \underset{˙}{\lor} r)))$
24	23	com23	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to (Y \neq \emptyset \to (S \in X \to \exists r \in Y S \underset{˙}{\leq} (S \underset{˙}{\lor} r)))$
25	24	imp	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land Y \neq \emptyset) \to (S \in X \to \exists r \in Y S \underset{˙}{\leq} (S \underset{˙}{\lor} r))$
26	25	ancld	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land Y \neq \emptyset) \to (S \in X \to (S \in X \land \exists r \in Y S \underset{˙}{\leq} (S \underset{˙}{\lor} r)))$
27		oveq1	$⊢ q = S \to q \underset{˙}{\lor} r = S \underset{˙}{\lor} r$
28	27	breq2d	$⊢ q = S \to (S \underset{˙}{\leq} (q \underset{˙}{\lor} r) \leftrightarrow S \underset{˙}{\leq} (S \underset{˙}{\lor} r))$
29	28	rexbidv	$⊢ q = S \to (\exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r) \leftrightarrow \exists r \in Y S \underset{˙}{\leq} (S \underset{˙}{\lor} r))$
30	29	rspcev	$⊢ (S \in X \land \exists r \in Y S \underset{˙}{\leq} (S \underset{˙}{\lor} r)) \to \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)$
31	26 30	syl6	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land Y \neq \emptyset) \to (S \in X \to \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))$
32	31	adantrl	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in X \to \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))$
33	8 32	jcad	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in X \to (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$
34		simpl3	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to Y \subseteq A$
35	34	sseld	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in Y \to S \in A)$
36		simpll1	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \land S \in Y) \to K \in Lat$
37		ssel2	$⊢ (X \subseteq A \land q \in X) \to q \in A$
38	37	3ad2antl2	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \to q \in A$
39	38	adantr	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \land S \in Y) \to q \in A$
40	13 3	atbase	$⊢ q \in A \to q \in {Base}_{K}$
41	39 40	syl	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \land S \in Y) \to q \in {Base}_{K}$
42		simpl3	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \to Y \subseteq A$
43	42	sselda	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \land S \in Y) \to S \in A$
44	43 14	syl	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \land S \in Y) \to S \in {Base}_{K}$
45	13 1 2	latlej2	$⊢ (K \in Lat \land q \in {Base}_{K} \land S \in {Base}_{K}) \to S \underset{˙}{\leq} (q \underset{˙}{\lor} S)$
46	36 41 44 45	syl3anc	$⊢ (((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \land S \in Y) \to S \underset{˙}{\leq} (q \underset{˙}{\lor} S)$
47	46	ex	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \to (S \in Y \to S \underset{˙}{\leq} (q \underset{˙}{\lor} S))$
48	47	ancld	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \to (S \in Y \to (S \in Y \land S \underset{˙}{\leq} (q \underset{˙}{\lor} S)))$
49		oveq2	$⊢ r = S \to q \underset{˙}{\lor} r = q \underset{˙}{\lor} S$
50	49	breq2d	$⊢ r = S \to (S \underset{˙}{\leq} (q \underset{˙}{\lor} r) \leftrightarrow S \underset{˙}{\leq} (q \underset{˙}{\lor} S))$
51	50	rspcev	$⊢ (S \in Y \land S \underset{˙}{\leq} (q \underset{˙}{\lor} S)) \to \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)$
52	48 51	syl6	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land q \in X) \to (S \in Y \to \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))$
53	52	impancom	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in Y) \to (q \in X \to \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))$
54	53	ancld	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in Y) \to (q \in X \to (q \in X \land \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$
55	54	eximdv	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in Y) \to (\exists q q \in X \to \exists q (q \in X \land \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$
56		n0	$⊢ X \neq \emptyset \leftrightarrow \exists q q \in X$
57		df-rex	$⊢ \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r) \leftrightarrow \exists q (q \in X \land \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))$
58	55 56 57	3imtr4g	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land S \in Y) \to (X \neq \emptyset \to \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))$
59	58	impancom	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land X \neq \emptyset) \to (S \in Y \to \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))$
60	59	adantrr	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in Y \to \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))$
61	35 60	jcad	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in Y \to (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$
62	33 61	jaod	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to ((S \in X \lor S \in Y) \to (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$
63		pm4.72	$⊢ ((S \in X \lor S \in Y) \to (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \leftrightarrow ((S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)) \leftrightarrow ((S \in X \lor S \in Y) \lor (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))))$
64	62 63	sylib	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to ((S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)) \leftrightarrow ((S \in X \lor S \in Y) \lor (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r))))$
65	6 64	bitr4d	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in (X \underset{˙}{+} Y) \leftrightarrow (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$

Metamath Proof Explorer

Theorem elpaddn0

Proof