Metamath Proof Explorer


Theorem atcvrlln2

Description: An atom under a line is covered by it. (Contributed by NM, 2-Jul-2012)

Ref Expression
Hypotheses atcvrlln2.l ˙ = K
atcvrlln2.c C = K
atcvrlln2.a A = Atoms K
atcvrlln2.n N = LLines K
Assertion atcvrlln2 K HL P A X N P ˙ X P C X

Proof

Step Hyp Ref Expression
1 atcvrlln2.l ˙ = K
2 atcvrlln2.c C = K
3 atcvrlln2.a A = Atoms K
4 atcvrlln2.n N = LLines K
5 simpl3 K HL P A X N P ˙ X X N
6 simpl1 K HL P A X N P ˙ X K HL
7 eqid Base K = Base K
8 7 4 llnbase X N X Base K
9 5 8 syl K HL P A X N P ˙ X X Base K
10 eqid join K = join K
11 7 10 3 4 islln3 K HL X Base K X N q A r A q r X = q join K r
12 6 9 11 syl2anc K HL P A X N P ˙ X X N q A r A q r X = q join K r
13 5 12 mpbid K HL P A X N P ˙ X q A r A q r X = q join K r
14 simp1l1 K HL P A X N P ˙ X q A r A q r X = q join K r K HL
15 simp1l2 K HL P A X N P ˙ X q A r A q r X = q join K r P A
16 simp2l K HL P A X N P ˙ X q A r A q r X = q join K r q A
17 simp2r K HL P A X N P ˙ X q A r A q r X = q join K r r A
18 simp3l K HL P A X N P ˙ X q A r A q r X = q join K r q r
19 simp1r K HL P A X N P ˙ X q A r A q r X = q join K r P ˙ X
20 simp3r K HL P A X N P ˙ X q A r A q r X = q join K r X = q join K r
21 19 20 breqtrd K HL P A X N P ˙ X q A r A q r X = q join K r P ˙ q join K r
22 1 10 2 3 atcvrj2 K HL P A q A r A q r P ˙ q join K r P C q join K r
23 14 15 16 17 18 21 22 syl132anc K HL P A X N P ˙ X q A r A q r X = q join K r P C q join K r
24 23 20 breqtrrd K HL P A X N P ˙ X q A r A q r X = q join K r P C X
25 24 3exp K HL P A X N P ˙ X q A r A q r X = q join K r P C X
26 25 rexlimdvv K HL P A X N P ˙ X q A r A q r X = q join K r P C X
27 13 26 mpd K HL P A X N P ˙ X P C X