Theorem pclunN 40020

Description: The projective subspace closure of the union of two sets of atoms equals the closure of their projective sum. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)

Hypotheses

Ref	Expression
pclun.a	⊢ 𝐴 = (Atoms‘𝐾)
pclun.p	⊢ + = (+𝑃‘𝐾)
pclun.c	⊢ 𝑈 = (PCl‘𝐾)

Assertion

Ref	Expression
pclunN	⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) = (𝑈‘(𝑋 + 𝑌)))

Proof of Theorem pclunN

Step	Hyp	Ref	Expression
1		simp1 1136	. . 3 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝐾 ∈ 𝑉)
2		pclun.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
3		pclun.p	. . . 4 ⊢ + = (+𝑃‘𝐾)
4	2, 3	paddunssN 39930	. . 3 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ (𝑋 + 𝑌))
5	2, 3	paddssat 39936	. . 3 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴)
6		pclun.c	. . . 4 ⊢ 𝑈 = (PCl‘𝐾)
7	2, 6	pclssN 40016	. . 3 ⊢ ((𝐾 ∈ 𝑉 ∧ (𝑋 ∪ 𝑌) ⊆ (𝑋 + 𝑌) ∧ (𝑋 + 𝑌) ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) ⊆ (𝑈‘(𝑋 + 𝑌)))
8	1, 4, 5, 7	syl3anc 1373	. 2 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) ⊆ (𝑈‘(𝑋 + 𝑌)))
9		unss 4139	. . . . . . . . 9 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ↔ (𝑋 ∪ 𝑌) ⊆ 𝐴)
10	9	biimpi 216	. . . . . . . 8 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ 𝐴)
11	10	3adant1 1130	. . . . . . 7 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ 𝐴)
12	2, 6	pclssidN 40017	. . . . . . 7 ⊢ ((𝐾 ∈ 𝑉 ∧ (𝑋 ∪ 𝑌) ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌)))
13	1, 11, 12	syl2anc 584	. . . . . 6 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌)))
14		unss 4139	. . . . . 6 ⊢ ((𝑋 ⊆ (𝑈‘(𝑋 ∪ 𝑌)) ∧ 𝑌 ⊆ (𝑈‘(𝑋 ∪ 𝑌))) ↔ (𝑋 ∪ 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌)))
15	13, 14	sylibr 234	. . . . 5 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ⊆ (𝑈‘(𝑋 ∪ 𝑌)) ∧ 𝑌 ⊆ (𝑈‘(𝑋 ∪ 𝑌))))
16		simp2 1137	. . . . . 6 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ 𝐴)
17		simp3 1138	. . . . . 6 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑌 ⊆ 𝐴)
18		eqid 2733	. . . . . . . 8 ⊢ (PSubSp‘𝐾) = (PSubSp‘𝐾)
19	2, 18, 6	pclclN 40013	. . . . . . 7 ⊢ ((𝐾 ∈ 𝑉 ∧ (𝑋 ∪ 𝑌) ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) ∈ (PSubSp‘𝐾))
20	1, 11, 19	syl2anc 584	. . . . . 6 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) ∈ (PSubSp‘𝐾))
21	2, 18, 3	paddss 39967	. . . . . 6 ⊢ ((𝐾 ∈ 𝑉 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ (𝑈‘(𝑋 ∪ 𝑌)) ∈ (PSubSp‘𝐾))) → ((𝑋 ⊆ (𝑈‘(𝑋 ∪ 𝑌)) ∧ 𝑌 ⊆ (𝑈‘(𝑋 ∪ 𝑌))) ↔ (𝑋 + 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌))))
22	1, 16, 17, 20, 21	syl13anc 1374	. . . . 5 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ⊆ (𝑈‘(𝑋 ∪ 𝑌)) ∧ 𝑌 ⊆ (𝑈‘(𝑋 ∪ 𝑌))) ↔ (𝑋 + 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌))))
23	15, 22	mpbid 232	. . . 4 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌)))
24	2, 18	psubssat 39876	. . . . 5 ⊢ ((𝐾 ∈ 𝑉 ∧ (𝑈‘(𝑋 ∪ 𝑌)) ∈ (PSubSp‘𝐾)) → (𝑈‘(𝑋 ∪ 𝑌)) ⊆ 𝐴)
25	1, 20, 24	syl2anc 584	. . . 4 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) ⊆ 𝐴)
26	2, 6	pclssN 40016	. . . 4 ⊢ ((𝐾 ∈ 𝑉 ∧ (𝑋 + 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌)) ∧ (𝑈‘(𝑋 ∪ 𝑌)) ⊆ 𝐴) → (𝑈‘(𝑋 + 𝑌)) ⊆ (𝑈‘(𝑈‘(𝑋 ∪ 𝑌))))
27	1, 23, 25, 26	syl3anc 1373	. . 3 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 + 𝑌)) ⊆ (𝑈‘(𝑈‘(𝑋 ∪ 𝑌))))
28	18, 6	pclidN 40018	. . . 4 ⊢ ((𝐾 ∈ 𝑉 ∧ (𝑈‘(𝑋 ∪ 𝑌)) ∈ (PSubSp‘𝐾)) → (𝑈‘(𝑈‘(𝑋 ∪ 𝑌))) = (𝑈‘(𝑋 ∪ 𝑌)))
29	1, 20, 28	syl2anc 584	. . 3 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑈‘(𝑋 ∪ 𝑌))) = (𝑈‘(𝑋 ∪ 𝑌)))
30	27, 29	sseqtrd 3967	. 2 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 + 𝑌)) ⊆ (𝑈‘(𝑋 ∪ 𝑌)))
31	8, 30	eqssd 3948	1 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) = (𝑈‘(𝑋 + 𝑌)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ∪ cun 3896   ⊆ wss 3898  ‘cfv 6488  (class class class)co 7354  Atomscatm 39385  PSubSpcpsubsp 39618  +_𝑃cpadd 39917  PClcpclN 40009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-int 4900  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7357  df-oprab 7358  df-mpo 7359  df-1st 7929  df-2nd 7930  df-psubsp 39625  df-padd 39918  df-pclN 40010

This theorem is referenced by:  pclun2N  40021