Metamath Proof Explorer


Theorem cdleme41sn3a

Description: Show that [_ R / s ]_ N is under P .\/ Q when R .<_ ( P .\/ Q ) . (Contributed by NM, 19-Mar-2013)

Ref Expression
Hypotheses cdleme32.b B=BaseK
cdleme32.l ˙=K
cdleme32.j ˙=joinK
cdleme32.m ˙=meetK
cdleme32.a A=AtomsK
cdleme32.h H=LHypK
cdleme32.u U=P˙Q˙W
cdleme32.c C=s˙U˙Q˙P˙s˙W
cdleme32.d D=t˙U˙Q˙P˙t˙W
cdleme32.e E=P˙Q˙D˙s˙t˙W
cdleme32.i I=ιyB|tA¬t˙W¬t˙P˙Qy=E
cdleme32.n N=ifs˙P˙QIC
cdleme32a1.y Y=P˙Q˙D˙R˙t˙W
cdleme32a1.z Z=ιyB|tA¬t˙W¬t˙P˙Qy=Y
Assertion cdleme41sn3a KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QR/sN˙P˙Q

Proof

Step Hyp Ref Expression
1 cdleme32.b B=BaseK
2 cdleme32.l ˙=K
3 cdleme32.j ˙=joinK
4 cdleme32.m ˙=meetK
5 cdleme32.a A=AtomsK
6 cdleme32.h H=LHypK
7 cdleme32.u U=P˙Q˙W
8 cdleme32.c C=s˙U˙Q˙P˙s˙W
9 cdleme32.d D=t˙U˙Q˙P˙t˙W
10 cdleme32.e E=P˙Q˙D˙s˙t˙W
11 cdleme32.i I=ιyB|tA¬t˙W¬t˙P˙Qy=E
12 cdleme32.n N=ifs˙P˙QIC
13 cdleme32a1.y Y=P˙Q˙D˙R˙t˙W
14 cdleme32a1.z Z=ιyB|tA¬t˙W¬t˙P˙Qy=Y
15 simp2rl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QRA
16 simp3 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QR˙P˙Q
17 10 11 12 13 14 cdleme31sn1c RAR˙P˙QR/sN=Z
18 15 16 17 syl2anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QR/sN=Z
19 1 fvexi BV
20 nfv tKHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙Q
21 nfra1 ttA¬t˙W¬t˙P˙Qy=Y
22 nfcv _tB
23 21 22 nfriota _tιyB|tA¬t˙W¬t˙P˙Qy=Y
24 14 23 nfcxfr _tZ
25 nfcv _t˙
26 nfcv _tP˙Q
27 24 25 26 nfbr tZ˙P˙Q
28 27 a1i KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QtZ˙P˙Q
29 14 a1i KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QZ=ιyB|tA¬t˙W¬t˙P˙Qy=Y
30 breq1 Y=ZY˙P˙QZ˙P˙Q
31 30 adantl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QY=ZY˙P˙QZ˙P˙Q
32 simpl11 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QtA¬t˙W¬t˙P˙QKHLWH
33 simp12l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QPA
34 33 adantr KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QtA¬t˙W¬t˙P˙QPA
35 simp13l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QQA
36 35 adantr KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QtA¬t˙W¬t˙P˙QQA
37 15 adantr KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QtA¬t˙W¬t˙P˙QRA
38 simprl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QtA¬t˙W¬t˙P˙QtA
39 2 3 4 5 6 7 9 13 cdleme4a KHLWHPAQARAtAY˙P˙Q
40 32 34 36 37 38 39 syl131anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QtA¬t˙W¬t˙P˙QY˙P˙Q
41 40 ex KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QtA¬t˙W¬t˙P˙QY˙P˙Q
42 simp1 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QKHLWHPA¬P˙WQA¬Q˙W
43 simp2rr KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙Q¬R˙W
44 simp2l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QPQ
45 1 2 3 4 5 6 7 9 13 14 cdleme25cl KHLWHPA¬P˙WQA¬Q˙WRA¬R˙WPQR˙P˙QZB
46 42 15 43 44 16 45 syl122anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QZB
47 simp11 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QKHLWH
48 simp12 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QPA¬P˙W
49 simp13 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QQA¬Q˙W
50 2 3 5 6 cdlemb2 KHLWHPA¬P˙WQA¬Q˙WPQtA¬t˙W¬t˙P˙Q
51 47 48 49 44 50 syl121anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QtA¬t˙W¬t˙P˙Q
52 20 28 29 31 41 46 51 riotasv3d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QBVZ˙P˙Q
53 19 52 mpan2 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QZ˙P˙Q
54 18 53 eqbrtrd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QR/sN˙P˙Q